the format: exponent bits, fraction bits, bias
173def specRoundScaled =
174 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted sOffset : Nat .
175 (nat-eliminate (lambda unrestricted current : Nat . Nat)
176 (specRoundQuotient (nat-multiply numerator (specPow2 (nat-subtract specOffset sOffset))) denominator)
177 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
178 (specRoundQuotient numerator (nat-multiply denominator (specPow2 (nat-subtract sOffset specOffset))))))
179 (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.