the exact magnitude of a FINITE value as N / 2^150 (subnormal: 2f / 2^150;
normal: (2^23 + f) x 2^e / 2^150)
106def modelScaledMagnitude =
107 (lambda unrestricted bits : Nat .
108 (specSelect (specIsZero (modelExponent bits))
109 (nat-multiply 2 (modelFraction bits))
110 (nat-multiply (nat-add modelPow2Twenty3 (modelFraction bits)) (specPow2 (modelExponent bits)))))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.