def le32

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:171

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

171def le32(+d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {Nat.is_le(d, 32n) == True{} : Bool}:
172  N.lt_le(d, 32n, hd)