def number_next_other

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

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

50def number_next_other(+character: Char,
51                      +state: J.NumberState,
52                      evidence: {J.number_char(character) == J.NOther{} : J.NumberChar}) -> {J.number_next(state, character) == J.NumberInvalid{} : J.NumberState}:
53    match state:
54        case J.NumberInvalid{}: {==}
55        case J.NumberStart{}:
56            Equal.trans(J.NumberState, J.number_next(J.NumberStart{}, character), J.number_step(J.NOther{}, J.NumberStart{}), J.NumberInvalid{},
57                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberStart{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberStart{}))
58        case J.NumberMinus{}:
59            Equal.trans(J.NumberState, J.number_next(J.NumberMinus{}, character), J.number_step(J.NOther{}, J.NumberMinus{}), J.NumberInvalid{},
60                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberMinus{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberMinus{}))
61        case J.NumberZero{}:
62            Equal.trans(J.NumberState, J.number_next(J.NumberZero{}, character), J.number_step(J.NOther{}, J.NumberZero{}), J.NumberInvalid{},
63                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberZero{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberZero{}))
64        case J.NumberInteger{}:
65            Equal.trans(J.NumberState, J.number_next(J.NumberInteger{}, character), J.number_step(J.NOther{}, J.NumberInteger{}), J.NumberInvalid{},
66                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberInteger{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberInteger{}))
67        case J.NumberDot{}:
68            Equal.trans(J.NumberState, J.number_next(J.NumberDot{}, character), J.number_step(J.NOther{}, J.NumberDot{}), J.NumberInvalid{},
69                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberDot{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberDot{}))
70        case J.NumberFraction{}:
71            Equal.trans(J.NumberState, J.number_next(J.NumberFraction{}, character), J.number_step(J.NOther{}, J.NumberFraction{}), J.NumberInvalid{},
72                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberFraction{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberFraction{}))
73        case J.NumberExponent{}:
74            Equal.trans(J.NumberState, J.number_next(J.NumberExponent{}, character), J.number_step(J.NOther{}, J.NumberExponent{}), J.NumberInvalid{},
75                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponent{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponent{}))
76        case J.NumberExponentSign{}:
77            Equal.trans(J.NumberState, J.number_next(J.NumberExponentSign{}, character), J.number_step(J.NOther{}, J.NumberExponentSign{}), J.NumberInvalid{},
78                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponentSign{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponentSign{}))
79        case J.NumberExponentDigits{}:
80            Equal.trans(J.NumberState, J.number_next(J.NumberExponentDigits{}, character), J.number_step(J.NOther{}, J.NumberExponentDigits{}), J.NumberInvalid{},
81                Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponentDigits{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponentDigits{}))