the format: exponent bits, fraction bits, bias
168def specRoundScaled =
169 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted sOffset : Nat .
170 (nat-eliminate (lambda unrestricted current : Nat . Nat)
171 (specRoundQuotient (nat-multiply numerator (specPow2 (nat-subtract specOffset sOffset))) denominator)
172 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
173 (specRoundQuotient numerator (nat-multiply denominator (specPow2 (nat-subtract sOffset specOffset))))))
174 (specLessOrEqual specOffset sOffset)))))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.