def divmod
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as Naturalimport Base
333def divmod(+a: Nat, +b: Nat) -> Result<&2, &2, MathError, QuotRem>:
334 match b:
335 case 0n:
336 Fail{ZeroDivision{}}
337 case 1n+ +bp:
338 Done{QR{Nat.div(a, 1n+bp), Nat.mod(a, 1n+bp)}}
Uses (6)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/misc:divmod_done
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/misc:divmod_zero
- bend-collections-laws-crypto@1.0.0.0/spec/math/natural:DivMod.value
- bend-collections-laws-crypto@1.0.0.0/spec/math/natural:DivMod.zero_divisor
- bend-collections-laws-crypto@1.0.0.0/spec/math/generic:DivMod.agrees