JSONSourceProof.reverse_source_object_after_separator: 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 407-460 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=407&end_line=460

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_object_after_separator(+key: String,
                                          +value: J.Value,
                                          +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}),
        List.append(&2, J.Lexeme,
            List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
            J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> 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{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
        reverse_source_text("\"" ++ J.escape_string(key) ++ "\"",
            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.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
                J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
            List.append(&2, J.Lexeme,
                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{})),
                J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> 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{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
                List.append(&2, J.Lexeme, xs, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
                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{})),
                reverse_source_colon_value_tail(value, tail)),
            Equal.trans(List<&2, J.Lexeme>,
                List.append(&2, J.Lexeme,
                    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{})),
                    J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
                    List.append(&2, J.Lexeme,
                        List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
                        J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> 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{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
                LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
                    List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
                    J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
                Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
                    List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), xs),
                    List.append(&2, J.Lexeme,
                        List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
                        J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
                    List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
                        List.append(&2, J.Lexeme, J.Punctuation{':'} <> Nil{}, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
                    LP.append_assoc(J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{},
                        J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})))))

Uses (19):
  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=Base/base.bend&name=String.append
  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=escape_string
  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_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_colon_value_tail
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_task
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_text