def
definition
def or abbrev
padLeftZeros
show as:
view Lean formalization →
formal statement (Lean)
28def padLeftZeros (s : String) (len : Nat) : String :=
proof body
Definition body.
29 let deficit := if s.length ≥ len then 0 else len - s.length
30 let rec mkZeros (n : Nat) (acc : String) : String :=
31 match n with
32 | 0 => acc
33 | n+1 => mkZeros n ("0" ++ acc)
34 mkZeros deficit s
35
36/-- Render a rational q = n / m to a fixed d-decimal string. -/