AlphaGitHub
Source/Reference

Float32Exact

reference/numeric/Float32Exact.alpha

142 lines17 declarations6.4 KiBSHA-256 e0ea5c3a7c33
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 23–34

float32ExactBetween

Full file
a value known to lie in [lo, hi]: its binary32 when both ends round to it
23def float32ExactBetween =
24  (lambda unrestricted loN : Nat .
25    (lambda unrestricted loD : Nat .
26      (lambda unrestricted hiN : Nat .
27        (lambda unrestricted hiD : Nat .
28          (let unrestricted lo =
29            (float32ExactRational loN loD)
30            in
31            (let unrestricted hi =
32              (float32ExactRational hiN hiD)
33              in
34              (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.