def render_array_whole_decompose

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

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

672def render_array_whole_decompose(+head: J.Value,
673                                 +tail: List<&2, J.Value>,
674                                 +suffix: String) -> {J.render(J.Arr{head <> tail}, False{}, suffix) == "[" ++ (J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix))) : String}:
675    Equal.cong(String, String, text => "[" ++ text,
676        render_after_separator(J.Arr{head <> tail}, suffix),
677        J.render(head, False{}, SNil{}) ++
678            (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)),
679        render_after_separator_array_decompose(head, tail, suffix))