def fits
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as Commonimport Base
59# n < 2^k
60def fits(+k: Nat, +n: Nat) -> Bool:
61 Nat.is_eq(high(k, n), 0n)
Uses (4)
Used by (169)
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value:fit_all
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width:lt_of_fits
- bend-collections-laws-crypto@1.0.0.0/spec/math/f64:sign
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width:fits_of_lt
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width:low_fit
- …