def
definition
def or abbrev
ratToDecimal
show as:
view Lean formalization →
formal statement (Lean)
21def ratToDecimal (n : Int) (m : Nat) (d : Nat) : String :=
proof body
Definition body.
22 let sign := if n < 0 then "-" else ""
23 let nAbs : Nat := Int.natAbs n
24 if m = 0 then sign ++ "NaN" else
25 let scale := pow10 d
26 let scaled : Nat := (nAbs * scale) / m
27 let ip : Nat := scaled / scale
28 let fp : Nat := scaled % scale
29 let fpStr := padLeftZeros (toString fp) d
30 sign ++ toString ip ++ (if d = 0 then "" else "." ++ fpStr)
31
32end NumFmt
33
34/-- Compute φ^k as a fixed-decimal string using a high-precision rational φ.
35 Supports negative exponents by inversion. Deterministic and computable. -/