@[simp]

theorem Nat.isDigit_digitChar {n : Nat} : n.digitChar.isDigit = decide (n < 10)

@[simp]

theorem Nat.digitChar_eq_zero {n : Nat} : n.digitChar = '0' ↔ n = 0

@[simp]

theorem Nat.digitChar_eq_one {n : Nat} : n.digitChar = '1' ↔ n = 1

@[simp]

theorem Nat.digitChar_eq_two {n : Nat} : n.digitChar = '2' ↔ n = 2

@[simp]

theorem Nat.digitChar_eq_three {n : Nat} : n.digitChar = '3' ↔ n = 3

@[simp]

theorem Nat.digitChar_eq_four {n : Nat} : n.digitChar = '4' ↔ n = 4

@[simp]

theorem Nat.digitChar_eq_five {n : Nat} : n.digitChar = '5' ↔ n = 5

@[simp]

theorem Nat.digitChar_eq_six {n : Nat} : n.digitChar = '6' ↔ n = 6

@[simp]

theorem Nat.digitChar_eq_seven {n : Nat} : n.digitChar = '7' ↔ n = 7

@[simp]

theorem Nat.digitChar_eq_eight {n : Nat} : n.digitChar = '8' ↔ n = 8

@[simp]

theorem Nat.digitChar_eq_nine {n : Nat} : n.digitChar = '9' ↔ n = 9

@[simp]

theorem Nat.digitChar_eq_a {n : Nat} : n.digitChar = 'a' ↔ n = 10

@[simp]

theorem Nat.digitChar_eq_b {n : Nat} : n.digitChar = 'b' ↔ n = 11

@[simp]

theorem Nat.digitChar_eq_c {n : Nat} : n.digitChar = 'c' ↔ n = 12

@[simp]

theorem Nat.digitChar_eq_d {n : Nat} : n.digitChar = 'd' ↔ n = 13

@[simp]

theorem Nat.digitChar_eq_e {n : Nat} : n.digitChar = 'e' ↔ n = 14

@[simp]

theorem Nat.digitChar_eq_f {n : Nat} : n.digitChar = 'f' ↔ n = 15

@[simp]

theorem Nat.digitChar_eq_star {n : Nat} : n.digitChar = '*' ↔ 16 ≤ n

@[simp]

theorem Nat.zero_eq_digitChar {n : Nat} : '0' = n.digitChar ↔ n = 0

@[simp]

theorem Nat.one_eq_digitChar {n : Nat} : '1' = n.digitChar ↔ n = 1

@[simp]

theorem Nat.two_eq_digitChar {n : Nat} : '2' = n.digitChar ↔ n = 2

@[simp]

theorem Nat.three_eq_digitChar {n : Nat} : '3' = n.digitChar ↔ n = 3

@[simp]

theorem Nat.four_eq_digitChar {n : Nat} : '4' = n.digitChar ↔ n = 4

@[simp]

theorem Nat.five_eq_digitChar {n : Nat} : '5' = n.digitChar ↔ n = 5

@[simp]

theorem Nat.six_eq_digitChar {n : Nat} : '6' = n.digitChar ↔ n = 6

@[simp]

theorem Nat.seven_eq_digitChar {n : Nat} : '7' = n.digitChar ↔ n = 7

@[simp]

theorem Nat.eight_eq_digitChar {n : Nat} : '8' = n.digitChar ↔ n = 8

@[simp]

theorem Nat.nine_eq_digitChar {n : Nat} : '9' = n.digitChar ↔ n = 9

@[simp]

theorem Nat.a_eq_digitChar {n : Nat} : 'a' = n.digitChar ↔ n = 10

@[simp]

theorem Nat.b_eq_digitChar {n : Nat} : 'b' = n.digitChar ↔ n = 11

@[simp]

theorem Nat.c_eq_digitChar {n : Nat} : 'c' = n.digitChar ↔ n = 12

@[simp]

theorem Nat.d_eq_digitChar {n : Nat} : 'd' = n.digitChar ↔ n = 13

@[simp]

theorem Nat.e_eq_digitChar {n : Nat} : 'e' = n.digitChar ↔ n = 14

@[simp]

theorem Nat.f_eq_digitChar {n : Nat} : 'f' = n.digitChar ↔ n = 15

@[simp]

theorem Nat.star_eq_digitChar {n : Nat} : '*' = n.digitChar ↔ 16 ≤ n

theorem Nat.digitChar_ne {n : Nat} (c : Char) (h : (c != '0' && c != '1' && c != '2' && c != '3' && c != '4' && c != '5' && c != '6' && c != '7' && c != '8' && c != '9' && c != 'a' && c != 'b' && c != 'c' && c != 'd' && c != 'e' && c != 'f' && c != '*') = true) : n.digitChar ≠ c

Auxiliary theorem for Nat.reduceDigitCharEq simproc.

theorem Nat.toNat_digitChar_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat = 48 + n

theorem Nat.toNat_digitChar_sub_48_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat - 48 = n

theorem Nat.isDigit_of_mem_toDigits {b n : Nat} {c : Char} (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ b.toDigits n) : c.isDigit = true

@[simp]

theorem Nat.underscore_not_in_toDigits {n : Nat} : ¬'_' ∈ toDigits 10 n

theorem Nat.toDigits_of_lt_base {b n : Nat} (h : n < b) : b.toDigits n = [n.digitChar]

@[simp]

theorem Nat.toDigits_zero (b : Nat) : b.toDigits 0 = ['0']

theorem Nat.toDigits_append_toDigits {b n d : Nat} (hb : 1 < b) (hn : 0 < n) (hd : d < b) : b.toDigits n ++ b.toDigits d = b.toDigits (b * n + d)

theorem Nat.toDigits_of_base_le {b n : Nat} (hb : 1 < b) (h : b ≤ n) : b.toDigits n = b.toDigits (n / b) ++ [(n % b).digitChar]

theorem Nat.toDigits_eq_if {b n : Nat} (hb : 1 < b) : b.toDigits n = if n < b then [n.digitChar] else b.toDigits (n / b) ++ [(n % b).digitChar]

theorem Nat.length_toDigits_pos {b n : Nat} : 0 < (b.toDigits n).length

@[simp]

theorem Nat.toDigits_ne_nil {n b : Nat} : b.toDigits n ≠ []

theorem Nat.length_toDigits_le_iff {b n k : Nat} (hb : 1 < b) (h : 0 < k) : (b.toDigits n).length ≤ k ↔ n < b ^ k

theorem Nat.repr_eq_ofList_toDigits {n : Nat} : n.repr = String.ofList (toDigits 10 n)

@[simp]

theorem Nat.toList_repr {n : Nat} : n.repr.toList = toDigits 10 n

@[simp]

theorem Nat.repr_ne_empty {n : Nat} : n.repr ≠ ""

theorem Nat.toString_eq_ofList_toDigits {n : Nat} : toString n = String.ofList (toDigits 10 n)

@[simp]

theorem Nat.toString_eq_repr {n : Nat} : toString n = n.repr

@[simp]

theorem Nat.reprPrec_eq_repr {n i : Nat} : reprPrec n i = Std.Format.text n.repr

@[simp]

theorem Nat.repr_eq_repr {n : Nat} : repr n = Std.Format.text n.repr

theorem Nat.repr_of_lt {n : Nat} (h : n < 10) : n.repr = String.singleton n.digitChar

theorem Nat.repr_of_ge {n : Nat} (h : 10 ≤ n) : n.repr = (n / 10).repr ++ String.singleton (n % 10).digitChar

theorem Nat.repr_eq_repr_append_repr {n : Nat} (h : 10 ≤ n) : n.repr = (n / 10).repr ++ (n % 10).repr

theorem Nat.length_repr_pos {n : Nat} : 0 < n.repr.length

theorem Nat.length_repr_le_iff {n k : Nat} (h : 0 < k) : n.repr.length ≤ k ↔ n < 10 ^ k

def Nat.ofDigitChars (b : Nat) (l : List Char) (init : Nat) : Nat

Transforms a list of characters into a natural number, assuming that all characters are in the range from '0' to '9'.

Equations

• b.ofDigitChars l init = List.foldl (fun (sofar : Nat) (c : Char) => b * sofar + (c.toNat - '0'.toNat)) init l

theorem Nat.ofDigitChars_eq_foldl {b : Nat} {l : List Char} {init : Nat} : b.ofDigitChars l init = List.foldl (fun (sofar : Nat) (c : Char) => b * sofar + (c.toNat - '0'.toNat)) init l

@[simp]

theorem Nat.ofDigitChars_nil {b init : Nat} : b.ofDigitChars [] init = init

theorem Nat.ofDigitChars_cons {b : Nat} {c : Char} {cs : List Char} {init : Nat} : b.ofDigitChars (c :: cs) init = b.ofDigitChars cs (b * init + (c.toNat - '0'.toNat))

theorem Nat.ofDigitChars_cons_digitChar_of_lt_ten {b n : Nat} (hn : n < 10) {cs : List Char} {init : Nat} : b.ofDigitChars (n.digitChar :: cs) init = b.ofDigitChars cs (b * init + n)

theorem Nat.ofDigitChars_eq_ofDigitChars_zero {l : List Char} {init : Nat} : ofDigitChars 10 l init = 10 ^ l.length * init + ofDigitChars 10 l 0

theorem Nat.ofDigitChars_append {b : Nat} {l m : List Char} (init : Nat) : b.ofDigitChars (l ++ m) init = b.ofDigitChars m (b.ofDigitChars l init)

@[simp]

theorem Nat.ofDigitChars_replicate_zero {b init n : Nat} : b.ofDigitChars (List.replicate n '0') init = b ^ n * init

theorem Nat.ofDigitChars_toDigits {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : b.ofDigitChars (b.toDigits n) 0 = n

@[simp]

theorem Nat.ofDigitChars_ten_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n