def render_after_separator_array_decompose

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

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

613def render_after_separator_array_decompose(+head: J.Value,
614                                           +tail: List<&2, J.Value>,
615                                           +suffix: String) -> {render_after_separator(J.Arr{head <> tail}, suffix) == J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)) : String}:
616    Equal.trans(String,
617        render_after_separator(J.Arr{head <> tail}, suffix),
618        J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix),
619        J.render(head, False{}, SNil{}) ++
620            (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)),
621        Equal.sym(String,
622            J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix),
623            render_after_separator(J.Arr{head <> tail}, suffix),
624            render_append(head, False{}, SNil{}, J.render(J.Arr{tail}, True{}, suffix))),
625        Equal.cong(String, String, text => J.render(head, False{}, SNil{}) ++ text,
626            J.render(J.Arr{tail}, True{}, suffix),
627            separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix),
628            render_members_decompose(J.Arr{tail}, suffix)))