JSONNumberLexProof.number_char_action: 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 106-121 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=106&end_line=121

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

def number_char_action(+character: Char,
                       +class: J.NumberChar,
                       class_eq: {J.number_char(character) == class : J.NumberChar},
                       +tail: String,
                       +state: J.NumberState,
                       evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> {J.lex_outside_action(character, class) == J.LexRaw{} : J.LexAction}:
    match class:
        case J.NOther{}:
            Empty.absurd({J.lex_outside_action(character, J.NOther{}) == J.LexRaw{} : J.LexAction},
                invalid_valid_tail(tail, state, character, class_eq, evidence))
        case J.NMinus{}: {==}
        case J.NPlus{}: {==}
        case J.NDot{}: {==}
        case J.NExp{}: {==}
        case J.NZero{}: {==}
        case J.NDigit{}: {==}

Uses (12):
  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=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=NumberChar
  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_outside_action
  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_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=invalid_valid_tail