def digit

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/src/wide.bend:71

import Base

71def digit(p: Nat, b: Bool, prior: Division<p>) -> Division<1n+p>:
72  Div{q, r} = prior
73  digit_compare(p, q, U32.add(U32.mul(r, 2), bit_u32(b)))