JSONRenderLexProof.lex_array: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend as JSONRenderLexProof
Lines 422-460 of qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&start_line=422&end_line=460

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_SourceProof.bend as SP

def lex_array(+head: J.Value,
              +tail: List<&2, J.Value>,
              +mode: SP.RenderMode,
              +boundary: Boundary,
              +acc: List<&2, J.Lexeme>,
              head_lex: {J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)) == finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) : List<&2, J.Lexeme>},
              tail_lex: {J.lex_scan(SP.render_task(J.Arr{tail}, SP.RenderAfterSeparator{}, boundary_text(boundary)), J.Outside{}, SNil{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) == finish(boundary, push(J.Arr{tail}, SP.RenderAfterSeparator{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))) : List<&2, J.Lexeme>}) -> {J.lex_scan(SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(J.Arr{head <> tail}, mode, acc)) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        J.lex_scan(SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc),
        J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc),
        finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
        Equal.cong(String, List<&2, J.Lexeme>,
            x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
            SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)),
            prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))),
            render_array(head, tail, mode, boundary, acc)),
        Equal.trans(List<&2, J.Lexeme>,
            J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc),
            J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)),
            finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
            scan_prefix(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), acc),
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)),
                finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
                finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
                head_lex,
                Equal.trans(List<&2, J.Lexeme>,
                    finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
                    finish(boundary, push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))),
                    finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
                    array_resume(tail, boundary, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)), tail_lex),
                    Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
                        x => finish(boundary, x),
                        push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
                        push(J.Arr{head <> tail}, mode, acc),
                        Equal.sym(List<&2, J.Lexeme>,
                            push(J.Arr{head <> tail}, mode, acc),
                            push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
                            push_array(head, tail, mode, acc)))))))

Uses (24):
  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=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexMode
  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/libs/JSON.bend&name=lex_scan
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=Boundary
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=Container
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=array_continuation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=array_resume
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=boundary_text
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=finish
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=prefix_acc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=prefix_text
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=push
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=push_array
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=render_array
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=scan_prefix
  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=render_task