From 5cd5a1b3b66935e5f86b1f631da50b69d602f6e6 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 18 Jan 2025 00:40:54 +0900 Subject: [PATCH] =?UTF-8?q?Float=E3=81=AE=E3=82=B3=E3=83=BC=E3=83=89?= =?UTF-8?q?=E4=BE=8B=E3=81=AE=E5=87=BA=E6=89=80=E3=82=92=E6=98=8E=E7=A4=BA?= =?UTF-8?q?=E3=81=99=E3=82=8B=20Fixes=20#1330?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Float.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/LeanByExample/Type/Float.lean b/LeanByExample/Type/Float.lean index 32c17918..721b723d 100644 --- a/LeanByExample/Type/Float.lean +++ b/LeanByExample/Type/Float.lean @@ -40,7 +40,8 @@ import Batteries.Data.Rat.Float --# -- `1/10` にはならない！ /-- info: (3602879701896397 : Rat)/36028797018963968 -/ -#guard_msgs in #eval (0.1 : Float).toRat0 +#guard_msgs in + #eval (0.1 : Float).toRat0 -- 分母の数は2の冪乗になっている -- これは浮動小数点数が内部で2進数で表現されていることを裏付ける @@ -48,7 +49,7 @@ import Batteries.Data.Rat.Float --# let x := (0.1 : Float).toRat0.den 2 ^ Nat.log2 x = x -/- これでは誤差の存在はわかってもその大きさが分かりづらいので、10進数として正確な表現を出力してみましょう。 -/ +/- これでは誤差の存在はわかってもその大きさが分かりづらいので、10進数として正確な表現を出力してみましょう。[^float] -/ /-- 分母が2のベキであるような正の有理数を10進小数として表示する -/ def Rat.pow2ToBase10Pos (x : Rat) : String := @@ -103,3 +104,5 @@ def Float.toExactDecimal (x : Float) : String := x.toRat0.pow2ToBase10 /-- info: "0.299999999999999988897769753748434595763683319091796875" -/ #guard_msgs in #eval Float.toExactDecimal 0.3 + +/- [^float]: この浮動小数点数を正確に表示させる関数の実装例は、筆者が Zulip のスレッド "display all of a Float object" で Daniel Weber 氏に教えていただいたものに基づいています。 -/