JSONSourceProof.reverse_source_colon_value_tail: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSONSourceProof
Lines 380-405 of qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&start_line=380&end_line=405

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
import qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend as LP

def reverse_source_colon_value_tail(+value: J.Value,
                                    +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
        List.append(&2, J.Lexeme,
            List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
            J.Punctuation{':'} <> Nil{}),
        List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
            List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
        LP.reverse_cons(J.Lexeme, J.Punctuation{':'}, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
        Equal.trans(List<&2, J.Lexeme>,
            List.append(&2, J.Lexeme,
                List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
                J.Punctuation{':'} <> Nil{}),
            List.append(&2, J.Lexeme,
                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})),
                J.Punctuation{':'} <> Nil{}),
            List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
                List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
                List.append(&2, J.Lexeme, xs, J.Punctuation{':'} <> Nil{}),
                List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})),
                reverse_source_suffix(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
            LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
                reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=source
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=append_assoc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=reverse_cons
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=RenderMode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_suffix
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_task