fix test

src/Init/Data/Array/Lex/Basic.lean

@@ -8,6 +8,9 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Range
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace Array
 
 /--

src/Init/Data/List/Monadic.lean

@@ -11,6 +11,9 @@ import Init.Data.List.Attach
 # Lemmas about `List.mapM` and `List.forM`.
 -/
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat

src/Init/Data/List/Notation.lean

@@ -11,6 +11,9 @@ import Init.Data.Nat.Div.Basic
 -/
 
 set_option linter.missingDocs true -- keep it documented
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 open Decidable List
 
 /--

src/Init/Data/List/OfFn.lean

@@ -11,6 +11,9 @@ import Init.Data.Fin.Fold
 # Theorems about `List.ofFn`
 -/
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /--

src/Init/Data/List/Pairwise.lean

@@ -11,6 +11,9 @@ import Init.Data.List.Attach
 # Lemmas about `List.Pairwise` and `List.Nodup`.
 -/
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -169,7 +172,7 @@ theorem pairwise_flatten {L : List (List α)} :
     simp only [flatten, pairwise_append, IH, mem_flatten, exists_imp, and_imp, forall_mem_cons,
       pairwise_cons, and_assoc, and_congr_right_iff]
     rw [and_comm, and_congr_left_iff]
-    intros; exact ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩
+    intros; exact ⟨fun h l' b c d e => h c d e l' b, fun h c d e l' b => h l' b c d e⟩
 
 @[deprecated pairwise_flatten (since := "2024-10-14")] abbrev pairwise_join := @pairwise_flatten
 
@@ -206,10 +209,10 @@ theorem pairwise_reverse {l : List α} :
         simp
       · exact ⟨fun _ => h, Or.inr h⟩
 
-theorem Pairwise.drop {l : List α} {n : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop n) :=
+theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
   h.sublist (drop_sublist _ _)
 
-theorem Pairwise.take {l : List α} {n : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take n) :=
+theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
   h.sublist (take_sublist _ _)
 
 theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by
@@ -231,9 +234,9 @@ theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l
         apply h; exact hab.cons _
 
 theorem Pairwise.rel_of_mem_take_of_mem_drop
-    {l : List α} (h : l.Pairwise R) (hx : x ∈ l.take n) (hy : y ∈ l.drop n) : R x y := by
+    {l : List α} (h : l.Pairwise R) (hx : x ∈ l.take i) (hy : y ∈ l.drop i) : R x y := by
   apply pairwise_iff_forall_sublist.mp h
-  rw [← take_append_drop n l, sublist_append_iff]
+  rw [← take_append_drop i l, sublist_append_iff]
   refine ⟨[x], [y], rfl, by simpa, by simpa⟩
 
 theorem Pairwise.rel_of_mem_append

src/Init/Data/List/Perm.lean

@@ -18,6 +18,9 @@ another.
 The notation `~` is used for permutation equivalence.
 -/
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 open Nat
 
 namespace List
@@ -90,8 +93,8 @@ theorem Perm.append_left {t₁ t₂ : List α} : ∀ l : List α, t₁ ~ t₂
 theorem Perm.append {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂ :=
   (p₁.append_right t₁).trans (p₂.append_left l₂)
 
-theorem Perm.append_cons (a : α) {h₁ h₂ t₁ t₂ : List α} (p₁ : h₁ ~ h₂) (p₂ : t₁ ~ t₂) :
-    h₁ ++ a :: t₁ ~ h₂ ++ a :: t₂ := p₁.append (p₂.cons a)
+theorem Perm.append_cons (a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : r₁ ~ r₂) :
+    l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ := p₁.append (p₂.cons a)
 
 @[simp] theorem perm_middle {a : α} : ∀ {l₁ l₂ : List α}, l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
   | [], _ => .refl _
@@ -167,7 +170,7 @@ theorem Perm.singleton_eq (h : [a] ~ l) : [a] = l := singleton_perm.mp h
 theorem singleton_perm_singleton {a b : α} : [a] ~ [b] ↔ a = b := by simp
 
 theorem perm_cons_erase [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l ~ a :: l.erase a :=
-  let ⟨_l₁, _l₂, _, e₁, e₂⟩ := exists_erase_eq h
+  let ⟨_, _, _, e₁, e₂⟩ := exists_erase_eq h
   e₂ ▸ e₁ ▸ perm_middle
 
 theorem Perm.filterMap (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
@@ -216,7 +219,7 @@ theorem exists_perm_sublist {l₁ l₂ l₂' : List α} (s : l₁ <+ l₂) (p :
     | .cons₂ _ (.cons _ s) => exact ⟨y :: _, .rfl, (s.cons₂ _).cons _⟩
     | .cons₂ _ (.cons₂ _ s) => exact ⟨x :: y :: _, .swap .., (s.cons₂ _).cons₂ _⟩
   | trans _ _ IH₁ IH₂ =>
-    let ⟨m₁, pm, sm⟩ := IH₁ s
+    let ⟨_, pm, sm⟩ := IH₁ s
     let ⟨r₁, pr, sr⟩ := IH₂ sm
     exact ⟨r₁, pr.trans pm, sr⟩
 
@@ -510,15 +513,15 @@ theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
     exact fun h h₁ h₂ => h h₂ h₁
 
-theorem perm_insertIdx {α} (x : α) (l : List α) {n} (h : n ≤ l.length) :
-    insertIdx n x l ~ x :: l := by
-  induction l generalizing n with
+theorem perm_insertIdx {α} (x : α) (l : List α) {i} (h : i ≤ l.length) :
+    insertIdx i x l ~ x :: l := by
+  induction l generalizing i with
   | nil =>
-    cases n with
+    cases i with
     | zero => rfl
     | succ => cases h
   | cons _ _ ih =>
-    cases n with
+    cases i with
     | zero => simp [insertIdx]
     | succ =>
       simp only [insertIdx, modifyTailIdx]

src/Init/Data/List/Range.lean

@@ -14,6 +14,9 @@ Most of the results are deferred to `Data.Init.List.Nat.Range`, where more resul
 natural arithmetic are available.
 -/
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -71,7 +74,7 @@ theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step *
     rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
 
 theorem getElem?_range' (s step) :
-    ∀ {m n : Nat}, m < n → (range' s n step)[m]? = some (s + step * m)
+    ∀ {i j : Nat}, i < j → (range' s j step)[i]? = some (s + step * i)
   | 0, n + 1, _ => by simp [range'_succ]
   | m + 1, n + 1, h => by
     simp only [range'_succ, getElem?_cons_succ]
@@ -144,10 +147,10 @@ theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0
 theorem range_eq_range' (n : Nat) : range n = range' 0 n :=
   (range_loop_range' n 0).trans <| by rw [Nat.zero_add]
 
-theorem getElem?_range {m n : Nat} (h : m < n) : (range n)[m]? = some m := by
+theorem getElem?_range {i j : Nat} (h : i < j) : (range j)[i]? = some i := by
   simp [range_eq_range', getElem?_range' _ _ h]
 
-@[simp] theorem getElem_range {n : Nat} (m) (h : m < (range n).length) : (range n)[m] = m := by
+@[simp] theorem getElem_range {i : Nat} (j) (h : j < (range i).length) : (range i)[j] = j := by
   simp [range_eq_range']
 
 theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n) := by
@@ -220,7 +223,7 @@ theorem zipIdx_eq_nil_iff {l : List α} {n : Nat} : List.zipIdx l n = [] ↔ l =
 
 @[simp]
 theorem getElem?_zipIdx :
-    ∀ (l : List α) n m, (zipIdx l n)[m]? = l[m]?.map fun a => (a, n + m)
+    ∀ (l : List α) i j, (zipIdx l i)[j]? = l[j]?.map fun a => (a, i + j)
   | [], _, _ => rfl
   | _ :: _, _, 0 => by simp
   | _ :: l, n, m + 1 => by
@@ -300,7 +303,7 @@ theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.lengt
 
 @[deprecated getElem?_zipIdx (since := "2025-01-21"), simp]
 theorem getElem?_enumFrom :
-    ∀ n (l : List α) m, (enumFrom n l)[m]? = l[m]?.map fun a => (n + m, a)
+    ∀ i (l : List α) j, (enumFrom i l)[j]? = l[j]?.map fun a => (i + j, a)
   | _, [], _ => rfl
   | _, _ :: _, 0 => by simp
   | n, _ :: l, m + 1 => by

src/Init/Data/List/Sublist.lean

@@ -11,6 +11,9 @@ import Init.Data.List.TakeDrop
 # Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`.
 -/
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -22,14 +25,14 @@ variable [BEq α]
 @[simp] theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} :
     isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons₂]
 
-@[simp] theorem isPrefixOf_length_pos_nil {L : List α} (h : 0 < L.length) : isPrefixOf L [] = false := by
-  cases L <;> simp_all [isPrefixOf]
+@[simp] theorem isPrefixOf_length_pos_nil {l : List α} (h : 0 < l.length) : isPrefixOf l [] = false := by
+  cases l <;> simp_all [isPrefixOf]
 
 @[simp] theorem isPrefixOf_replicate {a : α} :
     isPrefixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a)) := by
   induction l generalizing n with
   | nil => simp
-  | cons h t ih =>
+  | cons _ _ ih =>
     cases n
     · simp
     · simp [replicate_succ, isPrefixOf_cons₂, ih, Nat.succ_le_succ_iff, Bool.and_left_comm]
@@ -568,9 +571,9 @@ theorem flatten_sublist_iff {L : List (List α)} {l} :
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
   decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
 
-protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ n, l₁.drop n <+ l₂.drop n
+protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ i, l₁.drop i <+ l₂.drop i
   | _, _, h, 0 => h
-  | _, _, h, n + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop n
+  | _, _, h, i + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop i
 
 /-! ### IsPrefix / IsSuffix / IsInfix -/
 
@@ -604,10 +607,10 @@ theorem infix_refl (l : List α) : l <:+: l := prefix_rfl.isInfix
 
 @[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
 
-theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨L₁, L₂, h⟩ => ⟨a :: L₁, L₂, h ▸ rfl⟩
+theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨l₁', l₂', h⟩ => ⟨a :: l₁', l₂', h ▸ rfl⟩
 
-theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨L₁, L₂, h⟩ =>
-  ⟨L₁, concat L₂ a, by simp [← h, concat_eq_append, append_assoc]⟩
+theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨l₁', l₂', h⟩ =>
+  ⟨l₁', concat l₂' a, by simp [← h, concat_eq_append, append_assoc]⟩
 
 theorem IsPrefix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
   | _, _, _, ⟨r₁, rfl⟩, ⟨r₂, rfl⟩ => ⟨r₁ ++ r₂, (append_assoc _ _ _).symm⟩
@@ -646,13 +649,13 @@ theorem eq_nil_of_infix_nil (h : l <:+: []) : l = [] := infix_nil.mp h
 theorem eq_nil_of_prefix_nil (h : l <+: []) : l = [] := prefix_nil.mp h
 theorem eq_nil_of_suffix_nil (h : l <:+ []) : l = [] := suffix_nil.mp h
 
-theorem IsPrefix.ne_nil {x y : List α} (h : x <+: y) (hx : x ≠ []) : y ≠ [] := by
+theorem IsPrefix.ne_nil {xs ys : List α} (h : xs <+: ys) (hx : xs ≠ []) : ys ≠ [] := by
   rintro rfl; exact hx <| List.prefix_nil.mp h
 
-theorem IsSuffix.ne_nil {x y : List α} (h : x <:+ y) (hx : x ≠ []) : y ≠ [] := by
+theorem IsSuffix.ne_nil {xs ys : List α} (h : xs <:+ ys) (hx : xs ≠ []) : ys ≠ [] := by
   rintro rfl; exact hx <| List.suffix_nil.mp h
 
-theorem IsInfix.ne_nil {x y : List α} (h : x <:+: y) (hx : x ≠ []) : y ≠ [] := by
+theorem IsInfix.ne_nil {xs ys : List α} (h : xs <:+: ys) (hx : xs ≠ []) : ys ≠ [] := by
   rintro rfl; exact hx <| List.infix_nil.mp h
 
 theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length :=
@@ -664,10 +667,10 @@ theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length :=
 theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length :=
   h.sublist.length_le
 
-theorem IsPrefix.getElem {x y : List α} (h : x <+: y) {n} (hn : n < x.length) :
-    x[n] = y[n]'(Nat.le_trans hn h.length_le) := by
+theorem IsPrefix.getElem {xs ys : List α} (h : xs <+: ys) {i} (hi : i < xs.length) :
+    xs[i] = ys[i]'(Nat.le_trans hi h.length_le) := by
   obtain ⟨_, rfl⟩ := h
-  exact (List.getElem_append_left hn).symm
+  exact (List.getElem_append_left hi).symm
 
 -- See `Init.Data.List.Nat.Sublist` for `IsSuffix.getElem`.
 
@@ -702,13 +705,13 @@ theorem IsSuffix.reverse : l₁ <:+ l₂ → reverse l₁ <+: reverse l₂ :=
 theorem IsPrefix.reverse : l₁ <+: l₂ → reverse l₁ <:+ reverse l₂ :=
   reverse_suffix.2
 
-theorem IsPrefix.head {x y : List α} (h : x <+: y) (hx : x ≠ []) :
-    x.head hx = y.head (h.ne_nil hx) := by
-  cases x <;> cases y <;> simp only [head_cons, ne_eq, not_true_eq_false] at hx ⊢
+theorem IsPrefix.head {l₁ l₂ : List α} (h : l₁ <+: l₂) (hx : l₁ ≠ []) :
+    l₁.head hx = l₂.head (h.ne_nil hx) := by
+  cases l₁ <;> cases l₂ <;> simp only [head_cons, ne_eq, not_true_eq_false] at hx ⊢
   all_goals (obtain ⟨_, h⟩ := h; injection h)
 
-theorem IsSuffix.getLast {x y : List α} (h : x <:+ y) (hx : x ≠ []) :
-    x.getLast hx = y.getLast (h.ne_nil hx) := by
+theorem IsSuffix.getLast {l₁ l₂ : List α} (h : l₁ <:+ l₂) (hx : l₁ ≠ []) :
+    l₁.getLast hx = l₂.getLast (h.ne_nil hx) := by
   rw [← head_reverse (by simpa), h.reverse.head,
     head_reverse (by rintro h; simp only [reverse_eq_nil_iff] at h; simp_all)]
 
@@ -839,8 +842,8 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
       simp [Nat.succ_lt_succ_iff, eq_comm]
 
 theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
-    l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ x (hx : x < l₁.length),
-      l₁[x] = l₂[x]'(Nat.lt_of_lt_of_le hx h) where
+    l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ i (hx : i < l₁.length),
+      l₁[i] = l₂[i]'(Nat.lt_of_lt_of_le hx h) where
   mp h := ⟨h.length_le, fun _ h' ↦ h.getElem h'⟩
   mpr h := by
     obtain ⟨hl, h⟩ := h
@@ -951,40 +954,40 @@ theorem infix_of_mem_flatten : ∀ {L : List (List α)}, l ∈ L → l <:+: flat
 theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
   prefix_append_right_inj [a]
 
-theorem take_prefix (n) (l : List α) : take n l <+: l :=
+theorem take_prefix (i) (l : List α) : take i l <+: l :=
   ⟨_, take_append_drop _ _⟩
 
-theorem drop_suffix (n) (l : List α) : drop n l <:+ l :=
+theorem drop_suffix (i) (l : List α) : drop i l <:+ l :=
   ⟨_, take_append_drop _ _⟩
 
-theorem take_sublist (n) (l : List α) : take n l <+ l :=
-  (take_prefix n l).sublist
+theorem take_sublist (i) (l : List α) : take i l <+ l :=
+  (take_prefix i l).sublist
 
-theorem drop_sublist (n) (l : List α) : drop n l <+ l :=
-  (drop_suffix n l).sublist
+theorem drop_sublist (i) (l : List α) : drop i l <+ l :=
+  (drop_suffix i l).sublist
 
-theorem take_subset (n) (l : List α) : take n l ⊆ l :=
-  (take_sublist n l).subset
+theorem take_subset (i) (l : List α) : take i l ⊆ l :=
+  (take_sublist i l).subset
 
-theorem drop_subset (n) (l : List α) : drop n l ⊆ l :=
-  (drop_sublist n l).subset
+theorem drop_subset (i) (l : List α) : drop i l ⊆ l :=
+  (drop_sublist i l).subset
 
-theorem mem_of_mem_take {l : List α} (h : a ∈ l.take n) : a ∈ l :=
-  take_subset n l h
+theorem mem_of_mem_take {l : List α} (h : a ∈ l.take i) : a ∈ l :=
+  take_subset _ _ h
 
-theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l :=
+theorem mem_of_mem_drop {i} {l : List α} (h : a ∈ l.drop i) : a ∈ l :=
   drop_subset _ _ h
 
-theorem drop_suffix_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <:+ drop m l := by
+theorem drop_suffix_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l <:+ drop i l := by
   rw [← Nat.sub_add_cancel h, Nat.add_comm, ← drop_drop]
   apply drop_suffix
 
 -- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`.
 
-theorem drop_sublist_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <+ drop m l :=
+theorem drop_sublist_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l <+ drop i l :=
   (drop_suffix_drop_left l h).sublist
 
-theorem drop_subset_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l ⊆ drop m l :=
+theorem drop_subset_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l ⊆ drop i l :=
   (drop_sublist_drop_left l h).subset
 
 theorem takeWhile_prefix (p : α → Bool) : l.takeWhile p <+: l :=

src/Init/Data/List/TakeDrop.lean

@@ -10,7 +10,8 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.take` and `List.drop`.
 -/
 
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -251,18 +252,18 @@ theorem dropLast_eq_take (l : List α) : l.dropLast = l.take (l.length - 1) := b
     induction l generalizing x <;> simp_all [dropLast]
 
 @[simp] theorem map_take (f : α → β) :
-    ∀ (L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
+    ∀ (l : List α) (i : Nat), (l.take i).map f = (l.map f).take i
   | [], i => by simp
   | _, 0 => by simp
-  | h :: t, n + 1 => by dsimp; rw [map_take f t n]
+  | _ :: tl, n + 1 => by dsimp; rw [map_take f tl n]
 
 @[simp] theorem map_drop (f : α → β) :
-    ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
+    ∀ (l : List α) (i : Nat), (l.drop i).map f = (l.map f).drop i
   | [], i => by simp
-  | L, 0 => by simp
-  | h :: t, n + 1 => by
+  | l, 0 => by simp
+  | _ :: tl, n + 1 => by
     dsimp
-    rw [map_drop f t]
+    rw [map_drop f tl]
 
 /-! ### takeWhile and dropWhile -/
 
@@ -395,7 +396,7 @@ theorem dropWhile_append {xs ys : List α} :
       if (xs.dropWhile p).isEmpty then ys.dropWhile p else xs.dropWhile p ++ ys := by
   induction xs with
   | nil => simp
-  | cons h t ih =>
+  | cons _ _ ih =>
     simp only [cons_append, dropWhile_cons]
     split <;> simp_all
 
@@ -440,13 +441,13 @@ theorem take_takeWhile {l : List α} (p : α → Bool) i :
 @[simp] theorem all_takeWhile {l : List α} : (l.takeWhile p).all p = true := by
   induction l with
   | nil => rfl
-  | cons h t ih => by_cases p h <;> simp_all
+  | cons h _ ih => by_cases p h <;> simp_all
 
 @[simp] theorem any_dropWhile {l : List α} :
     (l.dropWhile p).any (fun x => !p x) = !l.all p := by
   induction l with
   | nil => rfl
-  | cons h t ih => by_cases p h <;> simp_all
+  | cons h _ ih => by_cases p h <;> simp_all
 
 theorem replace_takeWhile [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool} (h : p a = p b) :
     (l.takeWhile p).replace a b = (l.replace a b).takeWhile p := by

src/Init/Data/List/ToArray.lean

@@ -15,19 +15,20 @@ import Init.Data.Array.Lex.Basic
 We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
 
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
-@[simp] theorem toList_set (a : Array α) (i x h) :
-    (a.set i x).toList = a.toList.set i x := rfl
+@[simp] theorem toList_set (xs : Array α) (i x h) :
+    (xs.set i x).toList = xs.toList.set i x := rfl
 
-theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
-    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
+theorem swap_def (xs : Array α) (i j : Nat) (hi hj) :
+    xs.swap i j hi hj = (xs.set i xs[j]).set j xs[i] (by simpa using hj) := by
   simp [swap]
 
-@[simp] theorem toList_swap (a : Array α) (i j : Nat) (hi hj) :
-    (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
+@[simp] theorem toList_swap (xs : Array α) (i j : Nat) (hi hj) :
+    (xs.swap i j hi hj).toList = (xs.toList.set i xs[j]).set j xs[i] := by simp [swap_def]
 
 end Array
 
@@ -35,16 +36,16 @@ namespace List
 
 open Array
 
-theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
-  cases a with
+theorem toArray_inj {as bs : List α} (h : as.toArray = bs.toArray) : as = bs := by
+  cases as with
   | nil => simpa using h
   | cons a as =>
-    cases b with
+    cases bs with
     | nil => simp at h
     | cons b bs => simpa using h
 
-@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
-    (a.toArrayAux b).size = b.size + a.length := by
+@[simp] theorem size_toArrayAux {as : List α} {xs : Array α} :
+    (as.toArrayAux xs).size = xs.size + as.length := by
   simp [size]
 
 -- This is not a `@[simp]` lemma because it is pushing `toArray` inwards.
@@ -367,8 +368,8 @@ theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.le
         rw [ih]
         simp_all
 
-theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
-    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs := by
+theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (xs : Array γ) :
+    zipWithAux as.toArray bs.toArray f (i + 1) xs = zipWithAux as.tail.toArray bs.tail.toArray f i xs := by
   rw [zipWithAux]
   conv => rhs; rw [zipWithAux]
   simp only [size_toArray, getElem_toArray, length_tail, getElem_tail]
@@ -379,16 +380,16 @@ theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β →
       rw [dif_neg (by omega)]
   · rw [dif_neg (by omega)]
 
-theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
-    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 cs := by
-  induction i generalizing as bs cs with
+theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (xs : Array γ) :
+    zipWithAux as.toArray bs.toArray f (i + 1) xs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 xs := by
+  induction i generalizing as bs xs with
   | zero => simp [zipWithAux_toArray_succ]
   | succ i ih =>
     rw [zipWithAux_toArray_succ, ih]
     simp
 
-theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) :
-    zipWithAux as.toArray bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray := by
+theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (xs : Array γ) :
+    zipWithAux as.toArray bs.toArray f 0 xs = xs ++ (List.zipWith f as bs).toArray := by
   rw [Array.zipWithAux]
   match as, bs with
   | [], _ => simp
@@ -405,8 +406,8 @@ theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List
     Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by
   simp [Array.zip, zipWith_toArray, zip]
 
-theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) :
-    zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by
+theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (xs : Array γ) :
+    zipWithAll.go f as.toArray bs.toArray i xs = xs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by
   unfold zipWithAll.go
   split <;> rename_i h
   · rw [zipWithAll_go_toArray]
@@ -502,12 +503,12 @@ abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
 theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
     (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
   simp [Array.flatMap]
-  suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
-      f a ++ List.foldl (fun bs a => bs ++ f a) cs as by
+  suffices ∀ xs, List.foldl (fun ys a => ys ++ f a) (f a ++ xs) as =
+      f a ++ List.foldl (fun ys a => ys ++ f a) xs as by
     erw [empty_append] -- Why doesn't this work via `simp`?
     simpa using this #[]
-  intro cs
-  induction as generalizing cs <;> simp_all
+  intro xs
+  induction as generalizing xs <;> simp_all
 
 @[simp] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by

src/Init/Data/List/ToArrayImpl.lean

@@ -6,18 +6,21 @@ Authors: Henrik Böving
 prelude
 import Init.Data.List.Basic
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 /--
 Auxiliary definition for `List.toArray`.
 `List.toArrayAux as r = r ++ as.toArray`
 -/
 @[inline_if_reduce]
 def List.toArrayAux : List α → Array α → Array α
-  | nil,       r => r
-  | cons a as, r => toArrayAux as (r.push a)
+  | nil,       xs => xs
+  | cons a as, xs => toArrayAux as (xs.push a)
 
 /-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
 @[inline, match_pattern, pp_nodot, export lean_list_to_array]
-def List.toArrayImpl (as : List α) : Array α :=
-  as.toArrayAux (Array.mkEmpty as.length)
+def List.toArrayImpl (xs : List α) : Array α :=
+  xs.toArrayAux (Array.mkEmpty xs.length)

src/Init/Data/List/Zip.lean

@@ -11,6 +11,9 @@ import Init.Data.Function
 # Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`.
 -/
 
+-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -20,7 +23,7 @@ open Nat
 /-! ### zipWith -/
 
 theorem zipWith_comm (f : α → β → γ) :
-    ∀ (la : List α) (lb : List β), zipWith f la lb = zipWith (fun b a => f a b) lb la
+    ∀ (as : List α) (bs : List β), zipWith f as bs = zipWith (fun b a => f a b) bs as
   | [], _ => List.zipWith_nil_right.symm
   | _ :: _, [] => rfl
   | _ :: as, _ :: bs => congrArg _ (zipWith_comm f as bs)
@@ -57,7 +60,7 @@ theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
     (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by
   induction l₁ generalizing l₂ i with
   | nil => rw [zipWith] <;> simp
-  | cons head tail =>
+  | cons _ _ =>
     cases l₂
     · simp
     · cases i <;> simp_all
@@ -122,25 +125,25 @@ theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Li
       · simp
       · simp [hl]
 
-theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by
-  induction l generalizing l' n with
+theorem take_zipWith : (zipWith f l l').take i = zipWith f (l.take i) (l'.take i) := by
+  induction l generalizing l' i with
   | nil => simp
   | cons hd tl hl =>
     cases l'
     · simp
-    · cases n
+    · cases i
       · simp
       · simp [hl]
 
 @[deprecated take_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_take := @take_zipWith
 
-theorem drop_zipWith : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n) := by
-  induction l generalizing l' n with
+theorem drop_zipWith : (zipWith f l l').drop i = zipWith f (l.drop i) (l'.drop i) := by
+  induction l generalizing l' i with
   | nil => simp
   | cons hd tl hl =>
     · cases l'
       · simp
-      · cases n
+      · cases i
         · simp
         · simp [hl]
 
@@ -152,17 +155,17 @@ theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
 
 @[deprecated tail_zipWith (since := "2024-07-28")] abbrev zipWith_distrib_tail := @tail_zipWith
 
-theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
-    (h : l.length = l'.length) :
-    zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by
-  induction l generalizing l' with
+theorem zipWith_append (f : α → β → γ) (l₁ l₁' : List α) (l₂ l₂' : List β)
+    (h : l₁.length = l₂.length) :
+    zipWith f (l₁ ++ l₁') (l₂ ++ l₂') = zipWith f l₁ l₂ ++ zipWith f l₁' l₂' := by
+  induction l₁ generalizing l₂ with
   | nil =>
-    have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
+    have : l₂ = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
     simp [this]
   | cons hl tl ih =>
-    cases l' with
+    cases l₂ with
     | nil => simp at h
-    | cons head tail =>
+    | cons _ _ =>
       simp only [length_cons, Nat.succ.injEq] at h
       simp [ih _ h]
 
@@ -199,7 +202,7 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li
       · simp only [zipWith_nil_right, nil_eq, append_eq_nil_iff, exists_and_left, and_imp]
         rintro rfl  rfl
         exact ⟨[], x₁ :: l₁, [], by simp⟩
-      · rintro ⟨w, x, y, z, h₁, _, h₃, rfl, rfl⟩
+      · rintro ⟨_, _, _, _, h₁, _, h₃, rfl, rfl⟩
         simp only [nil_eq, append_eq_nil_iff] at h₃
         obtain ⟨rfl, rfl⟩ := h₃
         simp
@@ -207,21 +210,21 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li
       simp only [zipWith_cons_cons]
       rw [cons_eq_append_iff]
       constructor
-      · rintro (⟨rfl, rfl⟩ | ⟨l₁'', rfl, h⟩)
+      · rintro (⟨rfl, rfl⟩ | ⟨_, rfl, h⟩)
         · exact ⟨[], x₁ :: l₁, [], x₂ :: l₂, by simp⟩
         · rw [ih₁] at h
-          obtain ⟨w, x, y, z, h, rfl, rfl, h', rfl⟩ := h
-          refine ⟨x₁ :: w, x, x₂ :: y, z, by simp [h, h']⟩
-      · rintro ⟨w, x, y, z, h₁, h₂, h₃, rfl, rfl⟩
+          obtain ⟨ws, xs, ys, zs, h, rfl, rfl, h', rfl⟩ := h
+          refine ⟨x₁ :: ws, xs, x₂ :: ys, zs, by simp [h, h']⟩
+      · rintro ⟨_, _, _, _, h₁, h₂, h₃, rfl, rfl⟩
         rw [cons_eq_append_iff] at h₂
         rw [cons_eq_append_iff] at h₃
-        obtain (⟨rfl, rfl⟩ | ⟨w', rfl, rfl⟩) := h₂
+        obtain (⟨rfl, rfl⟩ | ⟨_, rfl, rfl⟩) := h₂
         · simp only [zipWith_nil_left, true_and, nil_eq, reduceCtorEq, false_and, exists_const,
           or_false]
-          obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
+          obtain (⟨rfl, rfl⟩ | ⟨_, rfl, rfl⟩) := h₃
           · simp
           · simp_all
-        · obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
+        · obtain (⟨rfl, rfl⟩ | ⟨_, rfl, rfl⟩) := h₃
           · simp_all
           · simp_all [zipWith_append, Nat.succ_inj']
 
@@ -274,9 +277,9 @@ theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
 theorem zip_append :
     ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
       zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
-  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
-  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
-  | a :: l₁, r₁, b :: l₂, r₂, h => by
+  | [], _, _, _, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
+  | _, _, [], _, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
+  | _ :: _, _, _ :: _, _, h => by
     simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
 
 theorem zip_map' (f : α → β) (g : α → γ) :
@@ -448,9 +451,9 @@ theorem unzip_zip {l₁ : List α} {l₂ : List β} (h : length l₁ = length l
   · rw [unzip_zip_left (Nat.le_of_eq h)]
   · rw [unzip_zip_right (Nat.le_of_eq h.symm)]
 
-theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp.map Prod.fst = l)
-    (hr : lp.map Prod.snd = l') : lp = l.zip l' := by
-  rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
+theorem zip_of_prod {l : List α} {l' : List β} {xs : List (α × β)} (hl : xs.map Prod.fst = l)
+    (hr : xs.map Prod.snd = l') : xs = l.zip l' := by
+  rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
 theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 := by
   simp

src/Lean/Linter/List.lean

@@ -27,10 +27,10 @@ register_builtin_option linter.indexVariables : Bool := {
 }
 
 /--
-`set_option linter.listName true` enables a strict linter that
-validates that all `List` variables are named `l`, `xs`, `ys`, `zs`, `as`, or `bs` (optionally with a `'`, `₁`, or `₂` suffix).
+`set_option linter.listVariable true` enables a strict linter that
+validates that all `List`/`Array`/`Vector` variables use standardized names.
 -/
-register_builtin_option linter.listName : Bool := {
+register_builtin_option linter.listVariable : Bool := {
   defValue := false
   descr := "Validate that all `List`/`Array`/`Vector` variables use allowed names."
 }
@@ -52,6 +52,7 @@ def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
       | List.set _ _ i _ => [i]
       | List.insertIdx _ i _ _ => [i]
       | List.eraseIdx _ _ i _ => [i]
+      | List.zipIdx _ _ i => [i]
       | _ => []
       match idxs with
       | [] => none
@@ -72,7 +73,7 @@ def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) : IO (List (Synt
       -- Something is wrong here: sometimes `inferType` fails with an unknown fvar error,
       -- despite passing the local context here.
       -- We fail quietly by returning a `Unit` type.
-      let ty ← ctx.runMetaM ti.lctx do (Meta.inferType ti.expr) <|> pure (.const `Unit [])
+      let ty ← ctx.runMetaM ti.lctx do instantiateMVars (← (Meta.inferType ti.expr) <|> pure (.const `Unit []))
       if p ty then
         if let .fvar i := ti.expr then
           match ti.lctx.find? i with
@@ -110,47 +111,48 @@ builtin_initialize addLinter indexLinter
 
 /-- Strip optional suffixes from a binder name. -/
 def stripBinderName (s : String) : String :=
-  s.stripSuffix "'" |>.stripSuffix "₁" |>.stripSuffix "₂"
+  s.stripSuffix "'" |>.stripSuffix "₁" |>.stripSuffix "₂" |>.stripSuffix "₃"
 
 /-- Allowed names for `List` variables. -/
-def allowedListNames : List String := ["l", "xs", "ys", "zs", "as", "bs"]
+def allowedListNames : List String := ["l", "r", "s", "t", "tl", "ws", "xs", "ys", "zs", "as", "bs", "cs", "acc"]
 
 /-- Allowed names for `Array` variables. -/
-def allowedArrayNames : List String := ["xs", "ys", "zs", "as", "bs"]
+def allowedArrayNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs"]
 
 /-- Allowed names for `Vector` variables. -/
-def allowedVectorNames : List String := ["xs", "ys", "zs", "as", "bs"]
+def allowedVectorNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs"]
 
 /--
 A linter which validates that all `List`/`Array`/`Vector` variables use allowed names.
 -/
-def listNameLinter : Linter
+def listVariableLinter : Linter
   where run := withSetOptionIn fun stx => do
-    unless (← getOptions).get linter.listName.name false do return
+    unless (← getOptions).get linter.listVariable.name false do return
     if (← get).messages.hasErrors then return
     if ! (← getInfoState).enabled then return
     for t in ← getInfoTrees do
       if let .context _ _ := t then -- Only consider info trees with top-level context
         let binders ← binders t
-        for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `List do
+        for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `List do
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedListNames.contains n then
-            Linter.logLint linter.listName stx
-              m!"Forbidden variable appearing as a `List` name: use `l` instead of {n}"
+            unless (ty.getArg! 0).isAppOf `List && n == "L" do
+              Linter.logLint linter.listVariable stx
+                m!"Forbidden variable appearing as a `List` name: {n}"
         for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedArrayNames.contains n then
-            Linter.logLint linter.listName stx
-              m!"Forbidden variable appearing as a `Array` name: use `l` instead of {n}"
+            Linter.logLint linter.listVariable stx
+              m!"Forbidden variable appearing as a `Array` name: {n}"
         for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedVectorNames.contains n then
-            Linter.logLint linter.listName stx
-              m!"Forbidden variable appearing as a `Vector` name: use `l` instead of {n}"
+            Linter.logLint linter.listVariable stx
+              m!"Forbidden variable appearing as a `Vector` name: {n}"
 
-builtin_initialize addLinter listNameLinter
+builtin_initialize addLinter listVariableLinter
 
 end Lean.Linter.List

tests/lean/run/list_name_linter.lean

@@ -1,4 +1,4 @@
-set_option linter.listName true
+set_option linter.listVariable true
 
 #guard_msgs in
 example (l : List Nat) : l = l := rfl
@@ -13,34 +13,34 @@ example (l₁ : List Nat) : l₁ = l₁ := rfl
 example (l₂ : List Nat) : l₂ = l₂ := rfl
 
 /--
-warning: Forbidden variable appearing as a `List` name: use `l` instead of l₃
-note: this linter can be disabled with `set_option linter.listName false`
+warning: Forbidden variable appearing as a `List` name: l₄
+note: this linter can be disabled with `set_option linter.listVariable false`
 ---
-warning: Forbidden variable appearing as a `List` name: use `l` instead of l₃
-note: this linter can be disabled with `set_option linter.listName false`
+warning: Forbidden variable appearing as a `List` name: l₄
+note: this linter can be disabled with `set_option linter.listVariable false`
 -/
 #guard_msgs in
-example (l₃ : List Nat) : l₃ = l₃ := rfl
+example (l₄ : List Nat) : l₄ = l₄ := rfl
 
 #guard_msgs in
 example (xs : List Nat) : xs = xs := rfl
 
 /--
-warning: Forbidden variable appearing as a `List` name: use `l` instead of ps
-note: this linter can be disabled with `set_option linter.listName false`
+warning: Forbidden variable appearing as a `List` name: ps
+note: this linter can be disabled with `set_option linter.listVariable false`
 ---
-warning: Forbidden variable appearing as a `List` name: use `l` instead of ps
-note: this linter can be disabled with `set_option linter.listName false`
+warning: Forbidden variable appearing as a `List` name: ps
+note: this linter can be disabled with `set_option linter.listVariable false`
 -/
 #guard_msgs in
 example (ps : List Nat) : ps = ps := rfl
 
 /--
-warning: Forbidden variable appearing as a `Array` name: use `l` instead of l
-note: this linter can be disabled with `set_option linter.listName false`
+warning: Forbidden variable appearing as a `Array` name: l
+note: this linter can be disabled with `set_option linter.listVariable false`
 ---
-warning: Forbidden variable appearing as a `Array` name: use `l` instead of l
-note: this linter can be disabled with `set_option linter.listName false`
+warning: Forbidden variable appearing as a `Array` name: l
+note: this linter can be disabled with `set_option linter.listVariable false`
 -/
 #guard_msgs in
 example (l : Array Nat) : l = l := rfl