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)
155def specRoundQuotient =
156 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
157 (nat-add (nat-divide numerator denominator)
158 (specSelect
159 (nat-less-than denominator (nat-multiply 2 (nat-modulo numerator denominator)))
160 1
161 (specSelect
162 (specNot (nat-less-than (nat-multiply 2 (nat-modulo numerator denominator)) denominator))
163 (nat-modulo (nat-divide numerator denominator) 2)
164 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.