normal: a significand that rounded up to 2^(fractionBits+1) moves to the next binade;
the exponent field is e + bias = (eOffset + bias) - specOffset, added BEFORE the offset is
removed (a negative e would otherwise saturate to 0 and give the wrong binade: 0.1 read as 1.6);
beyond 2^exponentBits - 2 it is overflow
214def specRoundWithLimit =
215 (lambda unrestricted chunks : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
216 (nat-eliminate (lambda unrestricted current : Nat . (family SpecRounded))
217 (constructor SpecRounded SpecRoundedOf
218 (specRoundScaled numerator denominator (nat-subtract (specBinadeOffsetWithLimit chunks numerator denominator) fractionBits))
219 (specBinadeOffsetWithLimit chunks numerator denominator)
220 0)
221 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecRounded) .
222 (constructor SpecRounded SpecRoundedOf
223 (specRoundScaled numerator denominator (nat-subtract (nat-subtract (nat-add specOffset 1) bias) fractionBits))
224 (nat-subtract (nat-add specOffset 1) bias)
225 1)))
226 (nat-less-than (specBinadeOffsetWithLimit chunks numerator denominator) (nat-subtract (nat-add specOffset 1) bias))))))))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.