def digit_result

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/src/wide.bend:61

import Base

61def digit_result(p: Nat, q: Word(p), r: U32, subtract: Bool) -> Division<1n+p>:
62  match subtract:
63    case False{}:
64      Div{WCon{False{}, q}, r}
65    case True{}:
66      Div{WCon{True{}, q}, U32.sub(r, 1000000)}