~/jendhub

def proof_unique

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

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

30def proof_unique(+valid: Bool,
31                 +a: J.NumberProofFrom(valid),
32                 +b: J.NumberProofFrom(valid)) -> {a == b : J.NumberProofFrom(valid)}:
33    match valid:
34        case True{}:
35            match a b:
36                case Unit{} Unit{}: {==}
37        case False{}:
38            match a:

Uses (3)

Used by (1)