pith. machine review for the scientific record. sign in
def definition def or abbrev

ratToDecimal

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  37def ratToDecimal (n : Int) (m : Nat) (d : Nat) : String :=

proof body

Definition body.

  38  let sign := if n < 0 then "-" else ""
  39  let nAbs : Nat := Int.natAbs n
  40  if m = 0 then sign ++ "NaN" else
  41  let scale := pow10 d
  42  let scaled : Nat := (nAbs * scale) / m
  43  let ip : Nat := scaled / scale
  44  let fp : Nat := scaled % scale
  45  let fpStr := padLeftZeros (toString fp) d
  46  sign ++ toString ip ++ (if d = 0 then "" else "." ++ fpStr)
  47
  48end NumFmt
  49

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.