def div_million

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

import Base

75# Binary long division, processing the most significant bit first. The partial
76# remainder stays below 1,000,000; the next candidate fits in U32 (<2,000,000).
77def div_million(+n: Nat, w: Word(n)) -> Division<n>:
78  match n:
79    case 0n:
80      Div{WNil{}, 0}
81    case 1n+p:
82      match w:
83        case WCon{b, tail}:
84          digit(p, b, div_million(p, tail))