def number_char_action

qasim-bend-kit@0.1.0.2 · proof/JSON_NumberLexProof.bend:106

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

106def number_char_action(+character: Char,
107                       +class: J.NumberChar,
108                       class_eq: {J.number_char(character) == class : J.NumberChar},
109                       +tail: String,
110                       +state: J.NumberState,
111                       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}:
112    match class:
113        case J.NOther{}:
114            Empty.absurd({J.lex_outside_action(character, J.NOther{}) == J.LexRaw{} : J.LexAction},
115                invalid_valid_tail(tail, state, character, class_eq, evidence))
116        case J.NMinus{}: {==}
117        case J.NPlus{}: {==}
118        case J.NDot{}: {==}
119        case J.NExp{}: {==}
120        case J.NZero{}: {==}
121        case J.NDigit{}: {==}