English
For base 0, the digits of 0 are the empty list; in general, digits 0 n is a singleton when n > 0.
Русский
Для основания 0 цифры числа 0 — пустой список; в общем случае digits 0 n образует одноэлементный список при n > 0.
LaTeX
$$$\text{digits}(0,0)=\emptyset $, и если $n>0$ то $\text{digits}(0,n)$ имеет вид $[n]$.$$
Lean4
/-- `digits b n` gives the digits, in little-endian order,
of a natural number `n` in a specified base `b`.
In any base, we have `ofDigits b L = L.foldr (fun x y ↦ x + b * y) 0`.
* For any `2 ≤ b`, we have `l < b` for any `l ∈ digits b n`,
and the last digit is not zero.
This uniquely specifies the behaviour of `digits b`.
* For `b = 1`, we define `digits 1 n = List.replicate n 1`.
* For `b = 0`, we define `digits 0 n = [n]`, except `digits 0 0 = []`.
Note this differs from the existing `Nat.toDigits` in core, which is used for printing numerals.
In particular, `Nat.toDigits b 0 = ['0']`, while `digits b 0 = []`.
-/
def digits : ℕ → ℕ → List ℕ
| 0 => digitsAux0
| 1 => digitsAux1
| b + 2 => digitsAux (b + 2) (by simp)
