def number_prefix_mode

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

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

123def number_prefix_mode(+text: String,
124                       +state: J.NumberState,
125                       +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_mode(text, J.Outside{}) == J.Outside{} : J.LexMode}:
126    match text:
127        case SNil{}: {==}
128        case SCon{+head, +tail}:
129            Equal.trans(J.LexMode, W.prefix_mode(SCon{head, tail}, J.Outside{}),
130                W.prefix_mode(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{})), J.Outside{},
131                {==},
132                Equal.trans(J.LexMode,
133                    W.prefix_mode(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{})),
134                    W.prefix_mode(tail, J.Outside{}), J.Outside{},
135                    Equal.cong(J.LexAction, J.LexMode, action => W.prefix_mode(tail, W.after_mode(action, J.Outside{})),
136                        J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{},
137                        number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
138                    number_prefix_mode(tail, J.number_next(state, head), number_valid_cons(head, tail, state, evidence))))