JSONNumberLexProof.lex_number_before_punctuation: 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 368-395 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=368&end_line=395 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_before_punctuation(+first: Char, +number_tail: String, +punctuation: Char, +suffix: String, +acc: List<&2, J.Lexeme>, action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}, +evidence: {J.number_valid(SCon{first, number_tail}) == True{} : Bool}) -> {J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{first, number_tail}} <> acc) : List<&2, J.Lexeme>}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{first, SNil{}}, acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{first, number_tail}} <> acc), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), W.after_mode(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.Outside{}), W.after_reversed(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), first, SNil{}), W.after_acc(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), first, SNil{}, acc)), J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{first, SNil{}}, acc), W.lex_scan_step(first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), Equal.cong(J.LexAction, List<&2, J.Lexeme>, lex_action => J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), W.after_mode(lex_action, J.Outside{}), W.after_reversed(lex_action, first, SNil{}), W.after_acc(lex_action, first, SNil{}, acc)), J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.LexRaw{}, number_char_action(first, J.number_char(first), {==}, number_tail, J.NumberStart{}, evidence))), lex_number_delimited_tail(number_tail, J.number_next(J.NumberStart{}, first), first, SNil{}, SCon{first, SNil{}}, punctuation, suffix, acc, Equal.trans(String, String.reverse(SCon{first, SNil{}}), String.reverse(SNil{}) ++ SCon{first, SNil{}}, SCon{first, SNil{}}, S.reverse_cons(first, SNil{}), S.append_nil(SCon{first, SNil{}})), action, number_valid_cons(first, number_tail, J.NumberStart{}, evidence))) Uses (26): 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.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=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 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_NumberLexProof.bend&name=lex_number_delimited_tail 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_nil https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=reverse_cons