def u0

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:168

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U

168def u0(+a: U32, +e: {v(a) == 0n : Nat}) -> {a == 0 : U32}:
169  U.injective(a, 0, e)