def lex_certified_number_before_punctuation

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

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_PrimitiveProof.bend as P

397def lex_certified_number_before_punctuation(+text: String,
398                                            +certificate: J.NumberCert<text>,
399                                            +punctuation: Char,
400                                            +suffix: String,
401                                            +acc: List<&2, J.Lexeme>,
402                                            action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc) : List<&2, J.Lexeme>}:
403    match text:
404        case SNil{}:
405            Empty.absurd({J.lex_scan(SNil{} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) ==
406                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SNil{}} <> acc) : List<&2, J.Lexeme>},
407                false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, P.cert_valid(SNil{}, certificate))))
408        case SCon{head, tail}:
409            lex_number_before_punctuation(head, tail, punctuation, suffix, acc, action, P.cert_valid(text, certificate))