def lex_number_valid

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

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

203def lex_number_valid(+text: String,
204                     +state: J.NumberState,
205                     +reversed: String,
206                     +acc: List<&2, J.Lexeme>,
207                     +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>}:
208    match text:
209        case SNil{}: {==}
210        case SCon{+head, +tail}:
211            Equal.trans(List<&2, J.Lexeme>,
212                J.lex_scan(text, J.Outside{}, reversed, acc),
213                J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}),
214                plain_lexemes(text, reversed, acc),
215                Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, reversed, acc, action),
216                    J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
217                    number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
218                Equal.trans(List<&2, J.Lexeme>,
219                    J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}),
220                    J.lexemes(tail, J.Outside{}, SCon{head, reversed}, acc, J.lex_seed_action(tail, J.Outside{})),
221                    plain_lexemes(text, reversed, acc),
222                    {==},
223                    lex_number_valid(tail, J.number_next(state, head), SCon{head, reversed}, acc,
224                        number_valid_cons(head, tail, state, evidence))))