AlphaGitHub
Source/Reference

BinaryFloatModel

reference/numeric/BinaryFloatModel.alpha

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

def · lines 353–368

binaryFloatAdd

Full file
353def binaryFloatAdd =
354  (lambda unrestricted format : (family BinaryFloatFormat) .
355    (lambda unrestricted a : Nat .
356      (lambda unrestricted b : Nat .
357        (specSelect
358          (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
359          (binaryFloatNaNResult format a b)
360          (specSelect
361            (binaryFloatIsInfinite format a)
362            (specSelect
363              (modelAnd
364                (binaryFloatIsInfinite format b)
365                (specNot (specEqual (binaryFloatSign format a) (binaryFloatSign format b))))
366              (binaryFloatDefaultNaN format)
367              a)
368            (specSelect (binaryFloatIsInfinite format b) b (binaryFloatAddFinite format a 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.