JSONRenderLexProof.lex_object: 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 486-526 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=486&end_line=526

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_object(+key: String,
               +head: J.Value,
               +tail: List<&2, Sigma<&2, &2, String, k => 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(object_continuation(tail, boundary))), J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)) == finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))) : List<&2, J.Lexeme>}, tail_lex: {J.lex_scan(SP.render_task(J.Obj{tail}, SP.RenderAfterSeparator{}, boundary_text(boundary)), J.Outside{}, SNil{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))) == finish(boundary, push(J.Obj{tail}, SP.RenderAfterSeparator{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)))) : List<&2, J.Lexeme>}) -> {J.lex_scan(SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        J.lex_scan(SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc),
        J.lex_scan(prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))), J.Outside{}, SNil{}, acc),
        finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
        Equal.cong(String, List<&2, J.Lexeme>,
            x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
            SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)),
            prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))),
            render_object(key, head, tail, mode, boundary, acc)),
        Equal.trans(List<&2, J.Lexeme>,
            J.lex_scan(prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))), J.Outside{}, SNil{}, acc),
            J.lex_scan(J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), J.Outside{}, SNil{}, prefix_acc(ObjectKind{}, mode, acc)),
            finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
            scan_prefix(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), acc),
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), J.Outside{}, SNil{}, prefix_acc(ObjectKind{}, mode, acc)),
                J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)),
                finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
                scan_field(key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), prefix_acc(ObjectKind{}, mode, acc)),
                Equal.trans(List<&2, J.Lexeme>,
                    J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)),
                    finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
                    finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
                    head_lex,
                    Equal.trans(List<&2, J.Lexeme>,
                        finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
                        finish(boundary, push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)))),
                        finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
                        object_resume(tail, boundary, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)), tail_lex),
                        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
                            x => finish(boundary, x),
                            push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
                            push(J.Obj{(key, head) <> tail}, mode, acc),
                            Equal.sym(List<&2, J.Lexeme>,
                                push(J.Obj{(key, head) <> tail}, mode, acc),
                                push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
                                push_object(key, head, tail, mode, acc))))))))

Uses (29):
  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=Sigma
  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=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=escape_string
  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/libs/JSON.bend&name=render_object_field
  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=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=object_continuation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=object_resume
  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_object
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=render_object
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&name=scan_field
  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