def lex_array
qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:422
import qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend as JSONRenderLexProof
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
422def lex_array(+head: J.Value,
423 +tail: List<&2, J.Value>,
424 +mode: SP.RenderMode,
425 +boundary: Boundary,
426 +acc: List<&2, J.Lexeme>,
427 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>},
428 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>}:
429 Equal.trans(List<&2, J.Lexeme>,
430 J.lex_scan(SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc),
431 J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc),
432 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
433 Equal.cong(String, List<&2, J.Lexeme>,
434 x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
435 SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)),
436 prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))),
437 render_array(head, tail, mode, boundary, acc)),
438 Equal.trans(List<&2, J.Lexeme>,
439 J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc),
440 J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)),
441 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
442 scan_prefix(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), acc),
443 Equal.trans(List<&2, J.Lexeme>,
444 J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)),
445 finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
446 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
447 head_lex,
448 Equal.trans(List<&2, J.Lexeme>,
449 finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
450 finish(boundary, push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))),
451 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
452 array_resume(tail, boundary, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)), tail_lex),
453 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
454 x => finish(boundary, x),
455 push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
456 push(J.Arr{head <> tail}, mode, acc),
457 Equal.sym(List<&2, J.Lexeme>,
458 push(J.Arr{head <> tail}, mode, acc),
459 push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
460 push_array(head, tail, mode, acc)))))))