floor(N / M / 2^s) with the remainder tie test, s = sOffset - specOffset (either sign):
q = floor(num'/den'), round up when 2r > den' or (2r == den' and q odd)
160def specRoundQuotient =
161 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
162 (nat-add (nat-divide numerator denominator)
163 (specSelect
164 (nat-less-than denominator (nat-multiply 2 (nat-modulo numerator denominator)))
165 1
166 (specSelect
167 (specNot (nat-less-than (nat-multiply 2 (nat-modulo numerator denominator)) denominator))
168 (nat-modulo (nat-divide numerator denominator) 2)
169 0)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.