268def binaryFloatRoundBitsWithLimit =
269 (lambda unrestricted chunks : Nat .
270 (lambda unrestricted format : (family BinaryFloatFormat) .
271 (lambda unrestricted sign : Nat .
272 (lambda unrestricted numerator : Nat .
273 (lambda unrestricted denominator : Nat .
274 (specSelect
275 (specIsZero numerator)
276 (binaryFloatZeroOf format sign)
277 (eliminate
278 SpecResult
279 (lambda unrestricted current : (family SpecResult) . Nat)
280 (specAssemble
281 (binaryFloatExponentBits format)
282 (binaryFloatFractionBits format)
283 (binaryFloatBias format)
284 sign
285 (specRoundWithLimit
286 chunks
287 (binaryFloatFractionBits format)
288 (binaryFloatBias format)
289 numerator
290 denominator))
291 (branch SpecBits n . n)
292 (branch SpecOverflow . (binaryFloatInfinityOf format sign)))))))))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.