JSONNumberLexProof.lex_number_delimited_tail: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as JSONNumberLexProof
Lines 310-366 of qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&start_line=310&end_line=366

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_StringProof.bend as S
import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as W

def lex_number_delimited_tail(+text: String,
                              +state: J.NumberState,
                              +rev_head: Char,
                              +rev_tail: String,
                              +payload: String,
                              +punctuation: Char,
                              +suffix: String,
                              +acc: List<&2, J.Lexeme>,
                              reverse_buffer: {String.reverse(SCon{rev_head, rev_tail}) == payload : String},
                              action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
                              +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ text} <> acc) : List<&2, J.Lexeme>}:
    match text:
        case SNil{}:
            Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SCon{rev_head, rev_tail}, acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SNil{}} <> acc),
                Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SCon{rev_head, rev_tail}, acc),
                    J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.flush_lexeme(SCon{rev_head, rev_tail}, acc)),
                    J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc),
                    W.scan_punctuation_char(punctuation, suffix, SCon{rev_head, rev_tail}, acc, action),
                    Equal.trans(List<&2, J.Lexeme>, J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.flush_lexeme(SCon{rev_head, rev_tail}, acc)),
                        J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc),
                        J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc),
                        {==},
                        Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc),
                            String.reverse(SCon{rev_head, rev_tail}), payload, reverse_buffer))),
                Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc),
                    payload, payload ++ SNil{}, Equal.sym(String, payload ++ SNil{}, payload, S.append_nil(payload))))
        case SCon{+head, +tail}:
            Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc),
                J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SCon{head, tail}} <> acc),
                Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc),
                    J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix),
                        W.after_mode(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.Outside{}),
                        W.after_reversed(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), head, SCon{rev_head, rev_tail}),
                        W.after_acc(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), head, SCon{rev_head, rev_tail}, acc)),
                    J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
                    W.lex_scan_step(head, tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc),
                    Equal.cong(J.LexAction, List<&2, J.Lexeme>, lex_action => J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix),
                        W.after_mode(lex_action, J.Outside{}), W.after_reversed(lex_action, head, SCon{rev_head, rev_tail}),
                        W.after_acc(lex_action, head, SCon{rev_head, rev_tail}, acc)),
                        J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.LexRaw{},
                        number_char_action(head, J.number_char(head), {==}, tail, state, evidence))),
                Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
                    J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{(payload ++ SCon{head, SNil{}}) ++ tail} <> acc),
                    J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SCon{head, tail}} <> acc),
                    lex_number_delimited_tail(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, payload ++ SCon{head, SNil{}},
                        punctuation, suffix, acc,
                        Equal.trans(String, String.reverse(SCon{head, SCon{rev_head, rev_tail}}),
                            String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}}, payload ++ SCon{head, SNil{}},
                            S.reverse_cons(head, SCon{rev_head, rev_tail}),
                            Equal.cong(String, String, value => value ++ SCon{head, SNil{}}, String.reverse(SCon{rev_head, rev_tail}), payload, reverse_buffer)),
                        action, number_valid_cons(head, tail, state, evidence)),
                    Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc),
                        (payload ++ SCon{head, SNil{}}) ++ tail, payload ++ SCon{head, tail},
                        S.append_assoc(payload, SCon{head, SNil{}}, tail))))

Uses (30):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.reverse
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexAction
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexMode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberState
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=flush_lexeme
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_scan
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_seed_action
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_char
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_next
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_end
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=after_acc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=after_mode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=after_reversed
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=lex_scan_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=scan_punctuation_char
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_char_action
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_valid_cons
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_assoc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_nil
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=reverse_cons