def render_after_separator_object_decompose

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

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

630def render_after_separator_object_decompose(+key: String,
631                                            +value: J.Value,
632                                            +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>, +suffix: String) -> {render_after_separator(J.Obj{(key, value) <> tail}, suffix) == J.render_object_field(SNil{}, key, J.render(value, False{}, SNil{}) ++ (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix))) : String}:
633    Equal.cong(String, String, text => J.render_object_field(SNil{}, key, text),
634        J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
635        J.render(value, False{}, SNil{}) ++
636            (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
637        Equal.trans(String,
638            J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
639            J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
640            J.render(value, False{}, SNil{}) ++
641                (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)),
642            Equal.sym(String,
643                J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix),
644                J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)),
645                render_append(value, False{}, SNil{}, J.render(J.Obj{tail}, True{}, suffix))),
646            Equal.cong(String, String, text => J.render(value, False{}, SNil{}) ++ text,
647                J.render(J.Obj{tail}, True{}, suffix),
648                separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix),
649                render_members_decompose(J.Obj{tail}, suffix))))