JSONSourceProof.lex_atomic_value_source: 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 840-856 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=840&end_line=856

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_PrimitiveProof.bend as P
import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S
import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as Num
import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as W

def lex_atomic_value_source(+atom: AtomicValue) -> {J.lex_scan(J.stringify(atomic_value(atom)), J.Outside{}, SNil{}, Nil{}) == J.source(atomic_value(atom), False{}, Nil{}) : List<&2, J.Lexeme>}:
    match atom:
        case AtomicNull{}: {==}
        case AtomicTrue{}: {==}
        case AtomicFalse{}: {==}
        case AtomicNumber{text, certificate}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(J.stringify(J.Number{text, certificate}), J.Outside{}, SNil{}, Nil{}),
                J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
                J.source(J.Number{text, certificate}, False{}, Nil{}),
                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Outside{}, SNil{}, Nil{}),
                    J.stringify(J.Number{text, certificate}), text, S.append_nil(text)),
                Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
                    J.Payload{text} <> Nil{}, J.source(J.Number{text, certificate}, False{}, Nil{}),
                    Num.lex_number_payload(text, P.cert_valid(text, certificate)), {==}))
        case AtomicString{text}:
            W.lex_rendered_string(text)

Uses (17):
  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.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/libs/JSON.bend&name=source
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=stringify
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=lex_rendered_string
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=lex_number_payload
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=cert_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=AtomicValue
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=atomic_value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_nil