409def binaryFloatDivide =
410 (lambda unrestricted format : (family BinaryFloatFormat) .
411 (lambda unrestricted a : Nat .
412 (lambda unrestricted b : Nat .
413 (specSelect
414 (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
415 (binaryFloatNaNResult format a b)
416 (specSelect
417 (modelOr
418 (modelAnd (binaryFloatIsInfinite format a) (binaryFloatIsInfinite format b))
419 (modelAnd (binaryFloatIsZero format a) (binaryFloatIsZero format b)))
420 (binaryFloatDefaultNaN format)
421 (specSelect
422 (modelOr (binaryFloatIsInfinite format a) (binaryFloatIsZero format b))
423 (binaryFloatInfinityOf
424 format
425 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
426 (specSelect
427 (modelOr (binaryFloatIsInfinite format b) (binaryFloatIsZero format a))
428 (binaryFloatZeroOf
429 format
430 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
431 (binaryFloatRoundBits
432 format
433 (modelXor (binaryFloatSign format a) (binaryFloatSign format b))
434 (binaryFloatScaledMagnitude format a)
435 (binaryFloatScaledMagnitude format b)))))))))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.