proofs/lib/lemmas/spec/unsigned_division.bend

bend-collections-laws-containers@1.0.0.0 · 8 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as N
3
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)