def render_after_separator_array_single

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

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

723def render_after_separator_array_single(+head: J.Value,
724                                        +suffix: String) -> {render_after_separator(J.Arr{head <> Nil{}}, suffix) == render_task(head, RenderWhole{}, "]" ++ suffix) : String}:
725    Equal.trans(String,
726        render_after_separator(J.Arr{head <> Nil{}}, suffix),
727        J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix)),
728        render_task(head, RenderWhole{}, "]" ++ suffix),
729        render_after_separator_array_decompose(head, Nil{}, suffix),
730        Equal.trans(String,
731            J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix)),
732            J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
733            render_task(head, RenderWhole{}, "]" ++ suffix),
734            Equal.cong(String, String, text => J.render(head, False{}, SNil{}) ++ text,
735                separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix), "]" ++ suffix, {==}),
736            render_task_append(head, RenderWhole{}, SNil{}, "]" ++ suffix)))