def div32
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as W64import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
128# (a / d, a mod d) for d > 0: the high word natively, the low word by digits
129def div32(+a: W.U64, +d: U32) -> W.U64 & U32:
130 div32_t1(U32.div(hi(a), d), lo(a), dig_t(U32.to_nat(U32.mod(hi(a), d)), 65536n, dig1(lo(a))), U32.to_nat(d))
Uses (11)
Used by (17)
- bend-collections-laws-math@1.0.0.0/src/math/w64:dm_pick
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div:div32_quot
- bend-collections-laws-math@1.0.0.0/src/math/w64:isqrt_big
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr:sqr_root_v
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv:q_v
- …