def render_array_singleton_suffix

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

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

149def render_array_singleton_suffix(+head: J.Value,
150                                  +suffix: String) -> {J.render(J.Arr{head <> Nil{}}, False{}, suffix) == "[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ suffix)) : String}:
151    Equal.cong(String, String, text => "[" ++ text,
152        J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
153        J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
154        Equal.trans(String,
155            J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
156            J.render(head, False{}, "]") ++ suffix,
157            J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
158            Equal.sym(String, J.render(head, False{}, "]") ++ suffix,
159                J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
160                nested_render_append(head, J.Arr{Nil{}}, True{}, SNil{}, suffix,
161                    render_append(head, False{}, "]", suffix),
162                    render_append(J.Arr{Nil{}}, True{}, SNil{}, suffix))),
163            Equal.trans(String,
164                J.render(head, False{}, "]") ++ suffix,
165                (J.render(head, False{}, SNil{}) ++ "]") ++ suffix,
166                J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
167                Equal.cong(String, String, text => text ++ suffix,
168                    J.render(head, False{}, "]"), J.render(head, False{}, SNil{}) ++ "]",
169                    Equal.sym(String, J.render(head, False{}, SNil{}) ++ "]",
170                        J.render(head, False{}, "]"), render_append(head, False{}, SNil{}, "]"))),
171                S.append_assoc(J.render(head, False{}, SNil{}), "]", suffix))))