JSONNumberLexProof.number_valid_cons: 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 11-35 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=11&end_line=35

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

def number_valid_cons(+character: Char,
                      +tail: String,
                      +state: J.NumberState,
                      evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> {J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))) == True{} : Bool}:
    match state:
        case J.NumberInvalid{}:
            Empty.absurd({J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})) == True{} : Bool}, false_true(evidence))
        case J.NumberStart{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberStart{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberStart{})), True{}, {==}, evidence)
        case J.NumberMinus{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberMinus{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberMinus{})), True{}, {==}, evidence)
        case J.NumberZero{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberZero{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberZero{})), True{}, {==}, evidence)
        case J.NumberInteger{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberInteger{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberInteger{})), True{}, {==}, evidence)
        case J.NumberDot{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberDot{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberDot{})), True{}, {==}, evidence)
        case J.NumberFraction{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberFraction{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberFraction{})), True{}, {==}, evidence)
        case J.NumberExponent{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponent{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponent{})), True{}, {==}, evidence)
        case J.NumberExponentSign{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponentSign{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponentSign{})), True{}, {==}, evidence)
        case J.NumberExponentDigits{}:
            Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponentDigits{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponentDigits{})), True{}, {==}, evidence)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=NumberState
  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=false_true