- reprTuple : α → List Lean.Format → List Lean.Format
Instances
Equations
- Nat.toDigitsCore base 0 x x = x
- Nat.toDigitsCore base (Nat.succ fuel) x x = let d := Nat.digitChar (x % base); let n' := x / base; if n' = 0 then d :: x else Nat.toDigitsCore base fuel n' (d :: x)