JSONSourceProof.render_array_singleton_suffix: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSONSourceProof
Lines 149-171 of qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&start_line=149&end_line=171

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

def render_array_singleton_suffix(+head: J.Value,
                                  +suffix: String) -> {J.render(J.Arr{head <> Nil{}}, False{}, suffix) == "[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ suffix)) : String}:
    Equal.cong(String, String, text => "[" ++ text,
        J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
        J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
        Equal.trans(String,
            J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
            J.render(head, False{}, "]") ++ suffix,
            J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
            Equal.sym(String, J.render(head, False{}, "]") ++ suffix,
                J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)),
                nested_render_append(head, J.Arr{Nil{}}, True{}, SNil{}, suffix,
                    render_append(head, False{}, "]", suffix),
                    render_append(J.Arr{Nil{}}, True{}, SNil{}, suffix))),
            Equal.trans(String,
                J.render(head, False{}, "]") ++ suffix,
                (J.render(head, False{}, SNil{}) ++ "]") ++ suffix,
                J.render(head, False{}, SNil{}) ++ ("]" ++ suffix),
                Equal.cong(String, String, text => text ++ suffix,
                    J.render(head, False{}, "]"), J.render(head, False{}, SNil{}) ++ "]",
                    Equal.sym(String, J.render(head, False{}, SNil{}) ++ "]",
                        J.render(head, False{}, "]"), render_append(head, False{}, SNil{}, "]"))),
                S.append_assoc(J.render(head, False{}, SNil{}), "]", suffix))))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=render
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=nested_render_append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=render_append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_assoc