def number_prefix_acc

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

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

140def number_prefix_acc(+text: String,
141                      +state: J.NumberState,
142                      +reversed: String,
143                      +acc: List<&2, J.Lexeme>,
144                      +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_acc(text, J.Outside{}, reversed, acc) == acc : List<&2, J.Lexeme>}:
145    match text:
146        case SNil{}: {==}
147        case SCon{+head, +tail}:
148            Equal.trans(List<&2, J.Lexeme>, W.prefix_acc(SCon{head, tail}, J.Outside{}, reversed, acc),
149                W.prefix_acc(tail, J.Outside{}, SCon{head, reversed}, acc), acc,
150                Equal.trans(List<&2, J.Lexeme>,
151                    W.prefix_acc(SCon{head, tail}, J.Outside{}, reversed, acc),
152                    W.prefix_acc(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{}),
153                        W.after_reversed(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed),
154                        W.after_acc(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed, acc)),
155                    W.prefix_acc(tail, J.Outside{}, SCon{head, reversed}, acc),
156                    {==},
157                    Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => W.prefix_acc(tail, W.after_mode(action, J.Outside{}),
158                        W.after_reversed(action, head, reversed), W.after_acc(action, head, reversed, acc)),
159                        J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{},
160                        number_char_action(head, J.number_char(head), {==}, tail, state, evidence))),
161                number_prefix_acc(tail, J.number_next(state, head), SCon{head, reversed}, acc,
162                    number_valid_cons(head, tail, state, evidence)))