379def binaryFloatMultiply =
380 (lambda unrestricted format : (family BinaryFloatFormat) .
381 (lambda unrestricted a : Nat .
382 (lambda unrestricted b : Nat .
383 (specSelect
384 (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
385 (binaryFloatNaNResult format a b)
386 (specSelect
387 (modelOr
388 (modelAnd (binaryFloatIsInfinite format a) (binaryFloatIsZero format b))
389 (modelAnd (binaryFloatIsZero format a) (binaryFloatIsInfinite format b)))
390 (binaryFloatDefaultNaN format)
391 (specSelect
392 (modelOr (binaryFloatIsInfinite format a) (binaryFloatIsInfinite format b))
393 (binaryFloatInfinityOf
394 format
395 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
396 (specSelect
397 (modelOr (binaryFloatIsZero format a) (binaryFloatIsZero format b))
398 (binaryFloatZeroOf
399 format
400 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
401 (binaryFloatRoundBits
402 format
403 (modelXor (binaryFloatSign format a) (binaryFloatSign format b))
404 (nat-multiply
405 (binaryFloatScaledMagnitude format a)
406 (binaryFloatScaledMagnitude format b))
407 (binaryFloatProductDenominator format)))))))))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.