def quotient

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/spec/unsigned_division.bend:4

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as N

4# Mathematical division of the interpreted input. Matching the word before
5# interpreting it avoids eager unary expansion of fixed denominator constants;
6# this is not a binary-division algorithm or an implementation import.
7def quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
8  N.unsigned_quotient(n, word, d)