def step_fits

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

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

71# b + 256 z fits 8 + k bits (Horner's step)
72def step_fits(+k: Nat, +b: Nat, +z: Nat, +hb: {C.fits(8n, b) == True{} : Bool}, +hz: {C.fits(k, z) == True{} : Bool}) -> {C.fits(Nat.add(8n, k), Nat.add(b, C.shift(8n, z))) == True{} : Bool}:
73  WW.limbs_fit(8n, k, b, z, hb, hz)