~/bend-docscommunity

proofs/lib/lemmas/spec/unsigned_division.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/unsigned_division.bend as Unsigned_division

2 imports
import Base
import ./numeric.bend as N

Definitions

def quotient source · line 7 · raw

@n:Nat -> @word:Word(n) -> @d:U32 -> Word(n)

Mathematical division of the interpreted input. Matching the word before interpreting it avoids eager unary expansion of fixed denominator constants; this is not a binary-division algorithm or an implementation import.