From 92f0d31ed73353eff40f28f68a3f453d14112e1c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 7 Feb 2025 12:44:51 +1100 Subject: [PATCH] chore: linting List (#6970) --- src/Init/Data/Array/Lex/Basic.lean | 3 ++ src/Init/Data/List/Monadic.lean | 3 ++ src/Init/Data/List/Notation.lean | 3 ++ src/Init/Data/List/OfFn.lean | 3 ++ src/Init/Data/List/Pairwise.lean | 13 +++-- src/Init/Data/List/Perm.lean | 21 ++++---- src/Init/Data/List/Range.lean | 13 +++-- src/Init/Data/List/Sublist.lean | 77 +++++++++++++++------------- src/Init/Data/List/TakeDrop.lean | 21 ++++---- src/Init/Data/List/ToArray.lean | 51 +++++++++--------- src/Init/Data/List/ToArrayImpl.lean | 11 ++-- src/Init/Data/List/Zip.lean | 61 +++++++++++----------- src/Lean/Linter/List.lean | 38 +++++++------- tests/lean/run/list_name_linter.lean | 28 +++++----- 14 files changed, 190 insertions(+), 156 deletions(-) diff --git a/src/Init/Data/Array/Lex/Basic.lean b/src/Init/Data/Array/Lex/Basic.lean index 65d1bdfeab..1ad7e3efd6 100644 --- a/src/Init/Data/Array/Lex/Basic.lean +++ b/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 /-- diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean index 92b43444ee..3b02e5f522 100644 --- a/src/Init/Data/List/Monadic.lean +++ b/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 diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean index 4c3db6cd9e..090cf18e78 100644 --- a/src/Init/Data/List/Notation.lean +++ b/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 /-- diff --git a/src/Init/Data/List/OfFn.lean b/src/Init/Data/List/OfFn.lean index 79b965e25f..ba92457860 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/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 /-- diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean index a15f42bfc6..0818cae0d9 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/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 diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index 57fc5b45e7..03de9311aa 100644 --- a/src/Init/Data/List/Perm.lean +++ b/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] diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean index 2e0b524c49..3a3c7753c2 100644 --- a/src/Init/Data/List/Range.lean +++ b/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 diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 860ae0aa7f..64c5369790 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/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 := diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index d0d049c1d9..a4e7b08339 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/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 diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 92dca96851..5a692e1c8f 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/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 diff --git a/src/Init/Data/List/ToArrayImpl.lean b/src/Init/Data/List/ToArrayImpl.lean index 214364b5bb..186b743e99 100644 --- a/src/Init/Data/List/ToArrayImpl.lean +++ b/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) diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index 7c6ab01bd5..ab76da17d4 100644 --- a/src/Init/Data/List/Zip.lean +++ b/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 diff --git a/src/Lean/Linter/List.lean b/src/Lean/Linter/List.lean index 661ebc51e5..a3836ab8d1 100644 --- a/src/Lean/Linter/List.lean +++ b/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 diff --git a/tests/lean/run/list_name_linter.lean b/tests/lean/run/list_name_linter.lean index 40a0ed07cf..a53cee0e62 100644 --- a/tests/lean/run/list_name_linter.lean +++ b/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