def divmod_rem

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64dmrem.bend:62

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

62def divmod_rem(+a: WU.U64, +b: WU.U64, +hb: {X.is_zero(b) == False{} : Bool}) -> SW.DivMod.rem(a, b, hb):
63  match a b:
64    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
65      dmr(1n, {==}, al, ah, bl, bh, hb, U32.is_zero(bh), {==})