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
209def specRound =
210 (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
211 (nat-eliminate (lambda unrestricted current : Nat . (family SpecRounded))
212 (constructor SpecRounded SpecRoundedOf
213 (specRoundScaled numerator denominator (nat-subtract (specBinadeOffset numerator denominator) fractionBits))
214 (specBinadeOffset numerator denominator)
215 0)
216 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecRounded) .
217 (constructor SpecRounded SpecRoundedOf
218 (specRoundScaled numerator denominator (nat-subtract (nat-subtract (nat-add specOffset 1) bias) fractionBits))
219 (nat-subtract (nat-add specOffset 1) bias)
220 1)))
221 (nat-less-than (specBinadeOffset 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.