def bnd

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbytes.bend:60

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

60# every value in r fits k bits
61def bnd(+k: Nat, r: Maybe<&2, Nat>) -> Bool:
62  match r:
63    case Some{+n}:
64      C.fits(k, n)
65    case None{}:
66      True{}