Merge pull request #1050 from lean-ja/Seasawher/issue1049

Float が仮数と指数で表現されていることを示す

LeanByExample/Reference/Type/Float.lean

@@ -13,10 +13,22 @@ import Mathlib.Data.String.Defs --#
 
 #eval (-42.0 : Float)
 
-/- ## 誤差
+/- ## 内部実装
+
+浮動小数点数は、[IEEE 754](https://ja.wikipedia.org/wiki/IEEE_754) に従い内部的には符号 `s ∈ {0, 1}` と仮数(significand) `c : ℕ` と指数 `q : ℤ` の三つ組で表されています。これは `(-1)ˢ × c × 2 ^ q` として解釈されます。
+-/
 
-浮動小数点数は、[IEEE 754](https://ja.wikipedia.org/wiki/IEEE_754) に従い内部的には符号 `s ∈ {0, 1}` と仮数(significand) `c : ℕ` と指数 `q : ℤ` の三つ組で表されています。これは `(-1)ˢ × c × 2 ^ q` として解釈されます。特に、2進数として表現されていることになるので、一般に `Float` で10進数を正確に計算することはできません。
+-- `64 = 1 * 2⁶` なので、仮数部は 1 で指数は 6 になる
+#guard Float.toRatParts' 64.0 = some (1, 6)
 
+-- `6 = 3 * 2¹` なので、仮数部は 3 で指数は 1 になる
+#guard Float.toRatParts' 6.0 = some (3, 1)
+
+-- `0.5 = 1 * 2⁻¹` なので、仮数部は 1 で指数は -1 になる
+#guard Float.toRatParts' 0.5 = some (1, -1)
+
+/- ## 誤差
+特に、浮動小数点数は2進数として表現されているので、一般に `Float` で10進数を正確に計算することはできません。
 次のように `0.1 : Float` を表示させると気が付きませんが、これは表示の際に数値が丸められているためです。
 -/