AlphaGitHub
Source/Reference

BinaryFloatModel

reference/numeric/BinaryFloatModel.alpha

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

def · lines 99–105

binaryFloatRoundingChunks

Full file
A finite significand scaled to this denominator has at most fractionBits + exponentMask bits; an exact product has at most twice that. Include one complete chunk beyond integer division, before the residual bit scan.
99def binaryFloatRoundingChunks =
100  (lambda unrestricted format : (family BinaryFloatFormat) .
101    (nat-add
102      1
103      (nat-divide
104        (nat-multiply 2 (nat-add (binaryFloatFractionBits format) (binaryFloatExponentMask format)))
105        64)))

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.