JSONPrimitiveProof.number_route: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as JSONPrimitiveProof
Lines 47-59 of qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&start_line=47&end_line=59

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

def number_route(+text: String,
                 +valid: Bool,
                 +certificate: J.NumberCert<text>,
                 evidence: {J.number_valid(text) == valid : Bool}) -> {J.payload_number(text, valid, evidence) == Done{J.Number{text, certificate}} : R()}:
    match valid:
        case True{}:
            Equal.cong(J.NumberCert<text>, R(), c => Done{J.Number{text, c}},
                J.Certified{J.number_proof(text, evidence)}, certificate,
                cert_unique(text, J.Certified{J.number_proof(text, evidence)}, certificate))
        case False{}:
            absurd({J.payload_number(text, False{}, evidence) == Done{J.Number{text, certificate}} : R()},
                false_true(Equal.trans(Bool, False{}, J.number_valid(text), True{},
                    Equal.sym(Bool, J.number_valid(text), False{}, evidence), cert_valid(text, certificate))))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberCert
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_proof
  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/libs/JSON.bend&name=payload_number
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=absurd
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=cert_unique
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=cert_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=false_true