JSONNumberLexProof.lex_number_valid: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as JSONNumberLexProof
Lines 203-224 of qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&start_line=203&end_line=224

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

def lex_number_valid(+text: String,
                     +state: J.NumberState,
                     +reversed: String,
                     +acc: List<&2, J.Lexeme>,
                     +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, reversed, acc) == plain_lexemes(text, reversed, acc) : List<&2, J.Lexeme>}:
    match text:
        case SNil{}: {==}
        case SCon{+head, +tail}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(text, J.Outside{}, reversed, acc),
                J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}),
                plain_lexemes(text, reversed, acc),
                Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, reversed, acc, action),
                    J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
                    number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
                Equal.trans(List<&2, J.Lexeme>,
                    J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}),
                    J.lexemes(tail, J.Outside{}, SCon{head, reversed}, acc, J.lex_seed_action(tail, J.Outside{})),
                    plain_lexemes(text, reversed, acc),
                    {==},
                    lex_number_valid(tail, J.number_next(state, head), SCon{head, reversed}, acc,
                        number_valid_cons(head, tail, state, evidence))))

Uses (19):
  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=LexAction
  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=NumberState
  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=lex_seed_action
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lexemes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_char
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_next
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_end
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_char_action
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_valid_cons
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=plain_lexemes