JSONSourceProof.render_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 56-147 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=56&end_line=147

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_StringProof.bend as S

def render_append(+value: J.Value,
                  +members: Bool,
                  +prefix: String,
                  +suffix: String) -> {J.render(value, members, prefix) ++ suffix == J.render(value, members, prefix ++ suffix) : String}:
    match value:
        case J.Null{}: S.append_assoc("null", prefix, suffix)
        case J.Bool{truth}:
            match truth:
                case True{}: S.append_assoc("true", prefix, suffix)
                case False{}: S.append_assoc("false", prefix, suffix)
        case J.Number{lexeme, certificate}: S.append_assoc(lexeme, prefix, suffix)
        case J.Str{text}:
            Equal.cong(String, String, rest => SCon{'"', rest},
                (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix,
                J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)),
                Equal.trans(String,
                    (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix,
                    J.escape_string(text) ++ ((SCon{'"', SNil{}} ++ prefix) ++ suffix),
                    J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)),
                    S.append_assoc(J.escape_string(text), SCon{'"', SNil{}} ++ prefix, suffix),
                    Equal.cong(String, String, value => J.escape_string(text) ++ value,
                        (SCon{'"', SNil{}} ++ prefix) ++ suffix,
                        SCon{'"', SNil{}} ++ (prefix ++ suffix),
                        S.append_assoc(SCon{'"', SNil{}}, prefix, suffix))))
        case J.Arr{Nil{}}:
            match members:
                case False{}: S.append_assoc("[]", prefix, suffix)
                case True{}: S.append_assoc("]", prefix, suffix)
        case J.Arr{head <> tail}:
            match members:
                case False{}:
                    Equal.trans(String, ("[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix,
                        "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
                        "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
                        S.append_assoc("[", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix),
                        Equal.trans(String, "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
                            "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
                            "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
                            Equal.cong(String, String, text => "[" ++ text,
                                J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix,
                                J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
                                render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)),
                            Equal.cong(String, String, text => "[" ++ J.render(head, False{}, text),
                                J.render(J.Arr{tail}, True{}, prefix) ++ suffix,
                                J.render(J.Arr{tail}, True{}, prefix ++ suffix),
                                render_append(J.Arr{tail}, True{}, prefix, suffix))))
                case True{}:
                    Equal.trans(String, ("," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix,
                        "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
                        "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
                        S.append_assoc(",", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix),
                        Equal.trans(String, "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
                            "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
                            "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
                            Equal.cong(String, String, text => "," ++ text,
                                J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix,
                                J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
                                render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)),
                            Equal.cong(String, String, text => "," ++ J.render(head, False{}, text),
                                J.render(J.Arr{tail}, True{}, prefix) ++ suffix,
                                J.render(J.Arr{tail}, True{}, prefix ++ suffix),
                                render_append(J.Arr{tail}, True{}, prefix, suffix))))
        case J.Obj{Nil{}}:
            match members:
                case False{}: S.append_assoc("{}", prefix, suffix)
                case True{}: S.append_assoc("}", prefix, suffix)
        case J.Obj{(key, field_value) <> tail}:
            match members:
                case False{}:
                    Equal.trans(String,
                        J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix,
                        J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix),
                        J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))),
                        render_object_field_append("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix),
                        Equal.cong(String, String, text => J.render_object_field("{", key, text),
                            J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix,
                            J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)),
                            nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix,
                                render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix),
                                render_append(J.Obj{tail}, True{}, prefix, suffix))))
                case True{}:
                    Equal.trans(String,
                        J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix,
                        J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix),
                        J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))),
                        render_object_field_append(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix),
                        Equal.cong(String, String, text => J.render_object_field(",", key, text),
                            J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix,
                            J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)),
                            nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix,
                                render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix),
                                render_append(J.Obj{tail}, True{}, prefix, suffix))))

Uses (15):
  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=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=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=render
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=render_object_field
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=nested_render_append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=render_object_field_append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_assoc