AlphaGitHub
Source/Reference

BinaryFloatModel

reference/numeric/BinaryFloatModel.alpha

467 lines54 declarations18.3 KiBSHA-256 cc13dd71cf68
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 258–266

binaryFloatScaledMagnitude

Full file
258def binaryFloatScaledMagnitude =
259  (lambda unrestricted format : (family BinaryFloatFormat) .
260    (lambda unrestricted bits : Nat .
261      (specSelect
262        (specIsZero (binaryFloatExponent format bits))
263        (nat-multiply 2 (binaryFloatFraction format bits))
264        (nat-multiply
265          (nat-add (binaryFloatFractionBase format) (binaryFloatFraction format bits))
266          (specPow2 (binaryFloatExponent format 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.