JSONNumberLexProof.number_next_other: 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 50-81 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=50&end_line=81

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

def number_next_other(+character: Char,
                      +state: J.NumberState,
                      evidence: {J.number_char(character) == J.NOther{} : J.NumberChar}) -> {J.number_next(state, character) == J.NumberInvalid{} : J.NumberState}:
    match state:
        case J.NumberInvalid{}: {==}
        case J.NumberStart{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberStart{}, character), J.number_step(J.NOther{}, J.NumberStart{}), J.NumberInvalid{},
                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{}))
        case J.NumberMinus{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberMinus{}, character), J.number_step(J.NOther{}, J.NumberMinus{}), J.NumberInvalid{},
                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{}))
        case J.NumberZero{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberZero{}, character), J.number_step(J.NOther{}, J.NumberZero{}), J.NumberInvalid{},
                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{}))
        case J.NumberInteger{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberInteger{}, character), J.number_step(J.NOther{}, J.NumberInteger{}), J.NumberInvalid{},
                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{}))
        case J.NumberDot{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberDot{}, character), J.number_step(J.NOther{}, J.NumberDot{}), J.NumberInvalid{},
                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{}))
        case J.NumberFraction{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberFraction{}, character), J.number_step(J.NOther{}, J.NumberFraction{}), J.NumberInvalid{},
                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{}))
        case J.NumberExponent{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberExponent{}, character), J.number_step(J.NOther{}, J.NumberExponent{}), J.NumberInvalid{},
                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{}))
        case J.NumberExponentSign{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberExponentSign{}, character), J.number_step(J.NOther{}, J.NumberExponentSign{}), J.NumberInvalid{},
                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{}))
        case J.NumberExponentDigits{}:
            Equal.trans(J.NumberState, J.number_next(J.NumberExponentDigits{}, character), J.number_step(J.NOther{}, J.NumberExponentDigits{}), J.NumberInvalid{},
                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{}))

Uses (9):
  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=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberChar
  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=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_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_other_invalid