JSONSourceProof.source_append: 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 279-360 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=279&end_line=360

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

def source_append(+value: J.Value,
                  +members: Bool,
                  +first: List<&2, J.Lexeme>,
                  +second: List<&2, J.Lexeme>) -> {J.source(value, members, List.append(&2, J.Lexeme, first, second)) == List.append(&2, J.Lexeme, J.source(value, members, first), second) : List<&2, J.Lexeme>}:
    match value:
        case J.Null{}: source_text_append("null", first, second)
        case J.Bool{truth}:
            match truth:
                case True{}: source_text_append("true", first, second)
                case False{}: source_text_append("false", first, second)
        case J.Number{lexeme, certificate}: source_text_append(lexeme, first, second)
        case J.Str{text}: source_text_append("\"" ++ J.escape_string(text) ++ "\"", first, second)
        case J.Arr{Nil{}}:
            match members:
                case False{}: {==}
                case True{}: {==}
        case J.Arr{head <> tail}:
            match members:
                case False{}:
                    Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'['} <> xs,
                        J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                        List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
                        Equal.trans(List<&2, J.Lexeme>,
                            J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                            J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)),
                            List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
                            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs),
                                J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
                                List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second),
                                source_append(J.Arr{tail}, True{}, first, second)),
                            source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second)))
                case True{}:
                    Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs,
                        J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                        List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
                        Equal.trans(List<&2, J.Lexeme>,
                            J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                            J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)),
                            List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
                            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs),
                                J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
                                List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second),
                                source_append(J.Arr{tail}, True{}, first, second)),
                            source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second)))
        case J.Obj{Nil{}}:
            match members:
                case False{}: {==}
                case True{}: {==}
        case J.Obj{(key, field_value) <> tail}:
            match members:
                case False{}:
                    Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'{'} <> xs,
                        J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))),
                        List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second),
                        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs),
                            J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                            List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
                            Equal.trans(List<&2, J.Lexeme>,
                                J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                                J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)),
                                List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
                                Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs),
                                    J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
                                    List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second),
                                    source_append(J.Obj{tail}, True{}, first, second)),
                                source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second))))
                case True{}:
                    Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs,
                        J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))),
                        List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second),
                        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs),
                            J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                            List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
                            Equal.trans(List<&2, J.Lexeme>,
                                J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
                                J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)),
                                List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
                                Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs),
                                    J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
                                    List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second),
                                    source_append(J.Obj{tail}, True{}, first, second)),
                                source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second))))

Uses (14):
  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=Sigma
  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/libs/JSON.bend&name=source_text
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=source_text_append