def number_route

qasim-bend-kit@0.1.0.2 · proof/JSON_PrimitiveProof.bend:47

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

47def number_route(+text: String,
48                 +valid: Bool,
49                 +certificate: J.NumberCert<text>,
50                 evidence: {J.number_valid(text) == valid : Bool}) -> {J.payload_number(text, valid, evidence) == Done{J.Number{text, certificate}} : R()}:
51    match valid:
52        case True{}:
53            Equal.cong(J.NumberCert<text>, R(), c => Done{J.Number{text, c}},
54                J.Certified{J.number_proof(text, evidence)}, certificate,
55                cert_unique(text, J.Certified{J.number_proof(text, evidence)}, certificate))
56        case False{}:
57            absurd({J.payload_number(text, False{}, evidence) == Done{J.Number{text, certificate}} : R()},
58                false_true(Equal.trans(Bool, False{}, J.number_valid(text), True{},
59                    Equal.sym(Bool, J.number_valid(text), False{}, evidence), cert_valid(text, certificate))))