JSONSourceProof.reverse_source_array_after_separator_whole: 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 538-567 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=538&end_line=567

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_ListProof.bend as LP

def reverse_source_array_after_separator_whole(+head: J.Value,
                                               +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        reverse_source_task(J.Arr{head <> tail}, RenderWhole{}),
        List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
            List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
        List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
        reverse_source_array_whole(head, tail),
        Equal.trans(List<&2, J.Lexeme>,
            List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
            List.append(&2, J.Lexeme,
                List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
                J.Punctuation{'['} <> Nil{}),
            List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
            Equal.sym(List<&2, J.Lexeme>,
                List.append(&2, J.Lexeme,
                    List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
                    J.Punctuation{'['} <> Nil{}),
                List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
                    List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
                LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
                    reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items =>
                List.append(&2, J.Lexeme, items, J.Punctuation{'['} <> Nil{}),
                List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
                reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
                Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
                    List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
                    reverse_source_array_after_separator(head, tail)))))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme
  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/proof/JSON_ListProof.bend&name=append_assoc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=RenderMode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_array_after_separator
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_array_whole
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_task