def
definition
def or abbrev
padLeftZeros
show as:
view Lean formalization →
formal statement (Lean)
12def padLeftZeros (s : String) (len : Nat) : String :=
proof body
Definition body.
13 let deficit := if s.length ≥ len then 0 else len - s.length
14 let rec mkZeros (n : Nat) (acc : String) : String :=
15 match n with
16 | 0 => acc
17 | n+1 => mkZeros n ("0" ++ acc)
18 mkZeros deficit s
19
20/-- Render a rational q = n / m to a fixed d-decimal string. -/