JSONSourceProof.render_object_whole_decompose: 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 651-670 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=651&end_line=670

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

def render_object_whole_decompose(+key: String,
                                  +value: J.Value,
                                  +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>, +suffix: String) -> {J.render(J.Obj{(key, value) <> tail}, False{}, suffix) == J.render_object_field("{", key, J.render(value, False{}, SNil{}) ++ (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix))) : String}:
    Equal.cong(String, String, text => J.render_object_field("{", key, text),
        J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
        J.render(value, False{}, SNil{}) ++
            (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
        Equal.trans(String,
            J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
            J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
            J.render(value, False{}, SNil{}) ++
                (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
            Equal.sym(String,
                J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
                J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
                render_append(value, False{}, SNil{}, J.render(J.Obj{tail}, True{}, suffix))),
            Equal.cong(String, String, text => J.render(value, False{}, SNil{}) ++ text,
                J.render(J.Obj{tail}, True{}, suffix),
                separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix),
                render_members_decompose(J.Obj{tail}, 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=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=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=render_after_separator
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=render_append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=render_members_decompose
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=separator_text