doc: state that Float is IEEE compliant (#3157)

Github discussion:
https://github.com/leanprover/lean4/pull/3147#discussion_r1446735973
This commit is contained in:
Geoffrey Irving 2024-01-10 12:16:42 +00:00 committed by GitHub
parent 4e16eb0476
commit 9069c538ad
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -26,7 +26,8 @@ opaque floatSpec : FloatSpec := {
decLe := fun _ _ => inferInstanceAs (Decidable True)
}
/-- Native floating point type, corresponding to 64-bit `double` in C. -/
/-- Native floating point type, corresponding to the IEEE 754 *binary64* format
(`double` in C or `f64` in Rust). -/
structure Float where
val : floatSpec.float