JSONNumberLexProof.lex_number_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 226-280 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=226&end_line=280 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 def lex_number_tail(+text: String, +state: J.NumberState, +rev_head: Char, +rev_tail: String, +first: Char, +prefix_tail: String, +reverse_prefix: {String.reverse(SCon{rev_head, rev_tail}) == SCon{first, prefix_tail} : String}, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}) == (J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}) : List<&2, J.Lexeme>}: match text: case SNil{}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SNil{}, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}), J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> Nil{}, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> Nil{}, {==}, Equal.trans(List<&2, J.Lexeme>, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> Nil{}, J.Payload{SCon{first, prefix_tail}} <> Nil{}, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> Nil{}, Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{}, String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix), Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{}, SCon{first, prefix_tail}, SCon{first, prefix_tail} ++ SNil{}, Equal.sym(String, SCon{first, prefix_tail} ++ SNil{}, SCon{first, prefix_tail}, S.append_nil(SCon{first, prefix_tail}))))) case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}), J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, J.LexRaw{}), J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}, Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, action), J.lex_seed_action(text, J.Outside{}), J.LexRaw{}, number_char_action(head, J.number_char(head), {==}, tail, state, evidence)), Equal.trans(List<&2, J.Lexeme>, J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, J.LexRaw{}), J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, Nil{}), J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}, {==}, Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, Nil{}), J.Payload{(SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail} <> Nil{}, J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}, lex_number_tail(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, first, prefix_tail ++ SCon{head, SNil{}}, Equal.trans(String, String.reverse(SCon{head, SCon{rev_head, rev_tail}}), String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}}, SCon{first, prefix_tail} ++ SCon{head, SNil{}}, S.reverse_cons(head, SCon{rev_head, rev_tail}), Equal.cong(String, String, x => x ++ SCon{head, SNil{}}, String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix)), number_valid_cons(head, tail, state, evidence)), Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{}, (SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail, SCon{first, prefix_tail} ++ text, S.append_assoc(SCon{first, prefix_tail}, SCon{head, SNil{}}, tail))))) Uses (25): 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=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=lexemes 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_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