JSONSourceProof.render_after_separator_array_decompose: 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 613-628 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=613&end_line=628

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

def render_after_separator_array_decompose(+head: J.Value,
                                           +tail: List<&2, J.Value>,
                                           +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}:
    Equal.trans(String,
        render_after_separator(J.Arr{head <> tail}, suffix),
        J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix),
        J.render(head, False{}, SNil{}) ++
            (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)),
        Equal.sym(String,
            J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix),
            render_after_separator(J.Arr{head <> tail}, suffix),
            render_append(head, False{}, SNil{}, J.render(J.Arr{tail}, True{}, suffix))),
        Equal.cong(String, String, text => J.render(head, False{}, SNil{}) ++ text,
            J.render(J.Arr{tail}, True{}, suffix),
            separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix),
            render_members_decompose(J.Arr{tail}, suffix)))

Uses (13):
  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=render_after_separator
  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_SourceProof.bend&name=render_members_decompose
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=separator_text