~/jendhub

def u32_eq_nat

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:176

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

176def u32_eq_nat(+a: U32, +b: U32) -> {U32.is_eq(a, b) == Nat.is_eq(v(a), v(b)) : Bool}:
177  Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, b), Nat.cmp(v(a), v(b)), U.u32_cmp(a, b))

Uses (11)

Used by (1)