def render_object_whole_decompose

qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:651

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

651def render_object_whole_decompose(+key: String,
652                                  +value: J.Value,
653                                  +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}:
654    Equal.cong(String, String, text => J.render_object_field("{", key, text),
655        J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
656        J.render(value, False{}, SNil{}) ++
657            (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
658        Equal.trans(String,
659            J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
660            J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
661            J.render(value, False{}, SNil{}) ++
662                (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
663            Equal.sym(String,
664                J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
665                J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
666                render_append(value, False{}, SNil{}, J.render(J.Obj{tail}, True{}, suffix))),
667            Equal.cong(String, String, text => J.render(value, False{}, SNil{}) ++ text,
668                J.render(J.Obj{tail}, True{}, suffix),
669                separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix),
670                render_members_decompose(J.Obj{tail}, suffix))))