AlphaGitHub
Source/Reference

Float32Exact

reference/numeric/Float32Exact.alpha

141 lines17 declarations6.3 KiBSHA-256 a0bb801f503e
Download exact fileView at revisionf5034773ad4bb52133

def · lines 22–33

float32ExactBetween

Full file
a value known to lie in [lo, hi]: its binary32 when both ends round to it
22def float32ExactBetween =
23  (lambda unrestricted loN : Nat .
24    (lambda unrestricted loD : Nat .
25      (lambda unrestricted hiN : Nat .
26        (lambda unrestricted hiD : Nat .
27          (let unrestricted lo =
28            (float32ExactRational loN loD)
29            in
30            (let unrestricted hi =
31              (float32ExactRational hiN hiD)
32              in
33              (naturalSelect (naturalEqual lo hi) lo float32NotRounded)))))))

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.