From 9069c538ad4f2e205fbfa83603e2b6c7620f4241 Mon Sep 17 00:00:00 2001
From: Geoffrey Irving <irving@naml.us>
Date: Wed, 10 Jan 2024 12:16:42 +0000
Subject: [PATCH] doc: state that `Float` is IEEE compliant (#3157)

Github discussion:
https://github.com/leanprover/lean4/pull/3147#discussion_r1446735973
---
 src/Init/Data/Float.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index adab897c10..1469c6a888 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -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