From d9ab758af588c404b64b27cc59e5b63accd6f303 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 25 Feb 2025 10:34:01 +1100 Subject: [PATCH] chore: re-enable List variable linter (#7215) Turns back on the variable names linters across List/Array/Vector. --- src/Init/Data/Array/Attach.lean | 5 +++-- src/Init/Data/Array/Basic.lean | 4 ++-- src/Init/Data/Array/BasicAux.lean | 4 ++-- src/Init/Data/Array/BinSearch.lean | 2 +- src/Init/Data/Array/Bootstrap.lean | 4 ++-- src/Init/Data/Array/Count.lean | 4 ++-- src/Init/Data/Array/DecidableEq.lean | 4 ++-- src/Init/Data/Array/Erase.lean | 4 ++-- src/Init/Data/Array/Extract.lean | 4 ++-- src/Init/Data/Array/FinRange.lean | 4 ++-- src/Init/Data/Array/Find.lean | 4 ++-- src/Init/Data/Array/GetLit.lean | 4 ++-- src/Init/Data/Array/InsertIdx.lean | 4 ++-- src/Init/Data/Array/InsertionSort.lean | 4 ++-- src/Init/Data/Array/Lemmas.lean | 12 ++++++------ src/Init/Data/Array/Lex/Basic.lean | 4 ++-- src/Init/Data/Array/Lex/Lemmas.lean | 4 ++-- src/Init/Data/Array/MapIdx.lean | 4 ++-- src/Init/Data/Array/Mem.lean | 4 ++-- src/Init/Data/Array/Monadic.lean | 4 ++-- src/Init/Data/Array/OfFn.lean | 4 ++-- src/Init/Data/Array/Perm.lean | 4 ++-- src/Init/Data/Array/QSort.lean | 2 +- src/Init/Data/Array/Range.lean | 10 +++++----- src/Init/Data/Array/Set.lean | 4 ++-- src/Init/Data/Array/Subarray.lean | 2 +- src/Init/Data/Array/Subarray/Split.lean | 4 ++-- src/Init/Data/Array/TakeDrop.lean | 4 ++-- src/Init/Data/Array/Zip.lean | 6 +++--- src/Init/Data/List/Attach.lean | 4 ++-- src/Init/Data/List/Basic.lean | 4 ++-- src/Init/Data/List/BasicAux.lean | 4 ++-- src/Init/Data/List/Control.lean | 4 ++-- src/Init/Data/List/Count.lean | 4 ++-- src/Init/Data/List/Erase.lean | 4 ++-- src/Init/Data/List/FinRange.lean | 4 ++-- src/Init/Data/List/Find.lean | 4 ++-- src/Init/Data/List/Impl.lean | 4 ++-- src/Init/Data/List/Lemmas.lean | 4 ++-- src/Init/Data/List/Lex.lean | 4 ++-- src/Init/Data/List/MapIdx.lean | 4 ++-- src/Init/Data/List/MinMax.lean | 4 ++-- src/Init/Data/List/Monadic.lean | 4 ++-- src/Init/Data/List/Nat/BEq.lean | 4 ++-- src/Init/Data/List/Nat/Basic.lean | 4 ++-- src/Init/Data/List/Nat/Count.lean | 4 ++-- src/Init/Data/List/Nat/Erase.lean | 4 ++-- src/Init/Data/List/Nat/Find.lean | 4 ++-- src/Init/Data/List/Nat/InsertIdx.lean | 4 ++-- src/Init/Data/List/Nat/Modify.lean | 4 ++-- src/Init/Data/List/Nat/Pairwise.lean | 4 ++-- src/Init/Data/List/Nat/Perm.lean | 4 ++-- src/Init/Data/List/Nat/Range.lean | 4 ++-- src/Init/Data/List/Nat/Sublist.lean | 4 ++-- src/Init/Data/List/Nat/TakeDrop.lean | 8 ++++---- src/Init/Data/List/Notation.lean | 4 ++-- src/Init/Data/List/OfFn.lean | 4 ++-- src/Init/Data/List/Pairwise.lean | 4 ++-- src/Init/Data/List/Perm.lean | 4 ++-- src/Init/Data/List/Range.lean | 14 +++++++------- src/Init/Data/List/Sort/Basic.lean | 4 ++-- src/Init/Data/List/Sort/Impl.lean | 4 ++-- src/Init/Data/List/Sort/Lemmas.lean | 4 ++-- src/Init/Data/List/Sublist.lean | 4 ++-- src/Init/Data/List/TakeDrop.lean | 4 ++-- src/Init/Data/List/ToArray.lean | 4 ++-- src/Init/Data/List/ToArrayImpl.lean | 4 ++-- src/Init/Data/List/Zip.lean | 4 ++-- src/Init/Data/Vector/Count.lean | 6 ++++-- src/Init/Data/Vector/DecidableEq.lean | 4 ++-- src/Init/Data/Vector/Erase.lean | 4 ++-- src/Init/Data/Vector/Extract.lean | 4 ++-- src/Init/Data/Vector/FinRange.lean | 4 ++-- src/Init/Data/Vector/InsertIdx.lean | 4 ++-- src/Init/Data/Vector/Lemmas.lean | 6 ++++-- src/Init/Data/Vector/Lex.lean | 4 ++-- src/Init/Data/Vector/MapIdx.lean | 4 ++-- src/Init/Data/Vector/Monadic.lean | 4 ++-- src/Init/Data/Vector/OfFn.lean | 4 ++-- src/Init/Data/Vector/Range.lean | 4 ++-- src/Init/Data/Vector/Zip.lean | 4 ++-- src/Lean/Linter/List.lean | 7 +++++-- 82 files changed, 184 insertions(+), 176 deletions(-) diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index 4a6614e850..9676b349dc 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -8,8 +8,9 @@ import Init.Data.Array.Mem import Init.Data.Array.Lemmas import Init.Data.Array.Count import Init.Data.List.Attach --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. + +set_option linter.listVariables 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/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 594aab25c5..90cf6b6895 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -14,8 +14,8 @@ import Init.GetElem import Init.Data.List.ToArrayImpl import Init.Data.Array.Set --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. universe u v w diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index 7abcd10b0e..ba1ef50afd 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -8,8 +8,8 @@ import Init.Data.Array.Basic import Init.Data.Nat.Linear import Init.NotationExtra --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by simp only [push, mk.injEq] at h diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean index 01ff01d18d..5145813dc4 100644 --- a/src/Init/Data/Array/BinSearch.lean +++ b/src/Init/Data/Array/BinSearch.lean @@ -9,7 +9,7 @@ import Init.Data.Int.DivMod.Lemmas import Init.Omega universe u v --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. -- We do not use `linter.indexVariables` here as it is helpful to name the index variables as `lo`, `mid`, and `hi`. namespace Array diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index 8c9612e3fa..9608cb89e6 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -13,8 +13,8 @@ import Init.Data.List.TakeDrop This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Count.lean b/src/Init/Data/Array/Count.lean index ec3ac83cad..b389124f42 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -11,8 +11,8 @@ import Init.Data.List.Nat.Count # Lemmas about `Array.countP` and `Array.count`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index 4843637c7e..e383c7764a 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -9,8 +9,8 @@ import Init.Data.BEq import Init.Data.List.Nat.BEq import Init.ByCases --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Erase.lean b/src/Init/Data/Array/Erase.lean index ee5d7e3d0c..95a9a26a42 100644 --- a/src/Init/Data/Array/Erase.lean +++ b/src/Init/Data/Array/Erase.lean @@ -12,8 +12,8 @@ import Init.Data.List.Nat.Basic # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Extract.lean b/src/Init/Data/Array/Extract.lean index 1edfff89c7..1976c105e9 100644 --- a/src/Init/Data/Array/Extract.lean +++ b/src/Init/Data/Array/Extract.lean @@ -13,8 +13,8 @@ import Init.Data.List.Nat.TakeDrop This file follows the contents of `Init.Data.List.TakeDrop` and `Init.Data.List.Nat.TakeDrop`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open Nat namespace Array diff --git a/src/Init/Data/Array/FinRange.lean b/src/Init/Data/Array/FinRange.lean index 26be512ba2..c6e4279b4d 100644 --- a/src/Init/Data/Array/FinRange.lean +++ b/src/Init/Data/Array/FinRange.lean @@ -7,8 +7,8 @@ prelude import Init.Data.List.FinRange import Init.Data.Array.OfFn --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Find.lean b/src/Init/Data/Array/Find.lean index 965c619793..d5b896ee61 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -13,8 +13,8 @@ import Init.Data.Array.Range # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Array open Nat diff --git a/src/Init/Data/Array/GetLit.lean b/src/Init/Data/Array/GetLit.lean index b8e4374863..d95c8fced6 100644 --- a/src/Init/Data/Array/GetLit.lean +++ b/src/Init/Data/Array/GetLit.lean @@ -7,8 +7,8 @@ Authors: Leonardo de Moura prelude import Init.Data.Array.Basic --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/InsertIdx.lean b/src/Init/Data/Array/InsertIdx.lean index 2193474dd6..83d1b22e4f 100644 --- a/src/Init/Data/Array/InsertIdx.lean +++ b/src/Init/Data/Array/InsertIdx.lean @@ -13,8 +13,8 @@ import Init.Data.List.Nat.InsertIdx Proves various lemmas about `Array.insertIdx`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open Function diff --git a/src/Init/Data/Array/InsertionSort.lean b/src/Init/Data/Array/InsertionSort.lean index f7eca28b2a..1c2072563b 100644 --- a/src/Init/Data/Array/InsertionSort.lean +++ b/src/Init/Data/Array/InsertionSort.lean @@ -6,8 +6,8 @@ Authors: Leonardo de Moura prelude import Init.Data.Array.Basic --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. @[inline] def Array.insertionSort (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α := traverse xs 0 xs.size diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 336bf8adf0..ac3c972943 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -22,8 +22,8 @@ import Init.Data.List.ToArray ## Theorems about `Array`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Array @@ -833,9 +833,9 @@ theorem getElem?_set (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) (j : N cases xs simp -@[simp] theorem set_eq_empty_iff {xs : Array α} (n : Nat) (a : α) (h) : - xs.set n a = #[] ↔ xs = #[] := by - cases xs <;> cases n <;> simp [set] +@[simp] theorem set_eq_empty_iff {xs : Array α} (i : Nat) (a : α) (h) : + xs.set i a = #[] ↔ xs = #[] := by + cases xs <;> cases i <;> simp [set] theorem set_comm (a b : α) {i j : Nat} (xs : Array α) {hi : i < xs.size} {hj : j < (xs.set i a).size} (h : i ≠ j) : @@ -2021,7 +2021,7 @@ theorem flatten_eq_flatMap {xss : Array (Array α)} : flatten xss = xss.flatMap rw [← Function.comp_def, ← List.map_map, flatten_toArray_map] theorem flatten_filter_not_isEmpty {xss : Array (Array α)} : - flatten (xss.filter fun l => !l.isEmpty) = xss.flatten := by + flatten (xss.filter fun xs => !xs.isEmpty) = xss.flatten := by induction xss using array₂_induction simp [List.filter_map, Function.comp_def, List.flatten_filter_not_isEmpty] diff --git a/src/Init/Data/Array/Lex/Basic.lean b/src/Init/Data/Array/Lex/Basic.lean index a98be90a17..ccc9e0d759 100644 --- a/src/Init/Data/Array/Lex/Basic.lean +++ b/src/Init/Data/Array/Lex/Basic.lean @@ -8,8 +8,8 @@ import Init.Data.Array.Basic import Init.Data.Nat.Lemmas import Init.Data.Range --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index 51c38fea14..ad93603d97 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -7,8 +7,8 @@ prelude import Init.Data.Array.Lemmas import Init.Data.List.Lex --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index 07e32038ea..a9164f4eee 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -8,8 +8,8 @@ import Init.Data.Array.Lemmas import Init.Data.Array.Attach import Init.Data.List.MapIdx --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Mem.lean b/src/Init/Data/Array/Mem.lean index 3c38b9c164..d59053472c 100644 --- a/src/Init/Data/Array/Mem.lean +++ b/src/Init/Data/Array/Mem.lean @@ -8,8 +8,8 @@ import Init.Data.Array.Basic import Init.Data.Nat.Linear import Init.Data.List.BasicAux --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean index 061bffeb55..b59b4f7dec 100644 --- a/src/Init/Data/Array/Monadic.lean +++ b/src/Init/Data/Array/Monadic.lean @@ -12,8 +12,8 @@ import Init.Data.List.Monadic # Lemmas about `Array.forIn'` and `Array.forIn`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean index 7fdad7b349..88b046e4ed 100644 --- a/src/Init/Data/Array/OfFn.lean +++ b/src/Init/Data/Array/OfFn.lean @@ -11,8 +11,8 @@ import Init.Data.List.OfFn # Theorems about `Array.ofFn` -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Perm.lean b/src/Init/Data/Array/Perm.lean index a21e2f313a..2d2ab764df 100644 --- a/src/Init/Data/Array/Perm.lean +++ b/src/Init/Data/Array/Perm.lean @@ -7,8 +7,8 @@ prelude import Init.Data.List.Nat.Perm import Init.Data.Array.Lemmas --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/QSort.lean b/src/Init/Data/Array/QSort.lean index fab8b7d016..b4ee01fb3f 100644 --- a/src/Init/Data/Array/QSort.lean +++ b/src/Init/Data/Array/QSort.lean @@ -7,7 +7,7 @@ prelude import Init.Data.Vector.Basic import Init.Data.Ord --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. -- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc. namespace Array diff --git a/src/Init/Data/Array/Range.lean b/src/Init/Data/Array/Range.lean index 186b6b6247..af9abfc26a 100644 --- a/src/Init/Data/Array/Range.lean +++ b/src/Init/Data/Array/Range.lean @@ -15,8 +15,8 @@ import Init.Data.List.Nat.Range -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Array @@ -149,9 +149,9 @@ theorem range_succ (n : Nat) : range (succ n) = range n ++ #[n] := by dite_eq_ite] split <;> omega -theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by +theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by rw [← range'_eq_map_range] - simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm + simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm theorem reverse_range' (s n : Nat) : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by simp [← toList_inj, List.reverse_range'] @@ -164,7 +164,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp -@[simp] theorem take_range (m n : Nat) : take (range n) m = range (min m n) := by +@[simp] theorem take_range (i n : Nat) : take (range n) i = range (min i n) := by ext <;> simp @[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} : diff --git a/src/Init/Data/Array/Set.lean b/src/Init/Data/Array/Set.lean index 93f6f886f4..85c40e84ff 100644 --- a/src/Init/Data/Array/Set.lean +++ b/src/Init/Data/Array/Set.lean @@ -6,8 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro prelude import Init.Tactics --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. /-- diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index e5d656a434..aa50e66555 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import Init.Data.Array.Basic --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. universe u v w diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean index c94d90bb96..7fc6afe3d5 100644 --- a/src/Init/Data/Array/Subarray/Split.lean +++ b/src/Init/Data/Array/Subarray/Split.lean @@ -15,8 +15,8 @@ automation. Placing them in another module breaks an import cycle, because `omeg array library. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Subarray /-- diff --git a/src/Init/Data/Array/TakeDrop.lean b/src/Init/Data/Array/TakeDrop.lean index b0a8a35bd6..09d3c47c36 100644 --- a/src/Init/Data/Array/TakeDrop.lean +++ b/src/Init/Data/Array/TakeDrop.lean @@ -12,8 +12,8 @@ These lemmas are used in the internals of HashMap. They should find a new home and/or be reformulated. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Array/Zip.lean b/src/Init/Data/Array/Zip.lean index e73bd83781..9fea34d774 100644 --- a/src/Init/Data/Array/Zip.lean +++ b/src/Init/Data/Array/Zip.lean @@ -11,8 +11,8 @@ import Init.Data.List.Zip # Lemmas about `Array.zip`, `Array.zipWith`, `Array.zipWithAll`, and `Array.unzip`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Array @@ -114,7 +114,7 @@ theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (cs : A cases ds simp [List.map_zipWith] -theorem take_zipWith : (zipWith f as bs).take n = zipWith f (as.take n) (bs.take n) := by +theorem take_zipWith : (zipWith f as bs).take i = zipWith f (as.take i) (bs.take i) := by cases as cases bs simp [List.take_zipWith] diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index f1115771c6..976f22572b 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -8,8 +8,8 @@ import Init.Data.List.Count import Init.Data.Subtype import Init.BinderNameHint --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Basic.lean b/src/Init/Data/List/Basic.lean index baf19c78af..64c778720f 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -58,8 +58,8 @@ Further operations are defined in `Init.Data.List.BasicAux` -/ set_option linter.missingDocs true -- keep it documented --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 82a65493c7..0951c0cbcc 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -6,8 +6,8 @@ Author: Leonardo de Moura prelude import Init.Data.Nat.Linear --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. universe u diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 8fa6910812..018ed2b517 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -9,8 +9,8 @@ import Init.Control.Id import Init.Control.Lawful import Init.Data.List.Basic --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace List universe u v w u₁ u₂ diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index 3e22909d19..d0d20b680e 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -10,8 +10,8 @@ import Init.Data.List.Sublist # Lemmas about `List.countP` and `List.count`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Erase.lean b/src/Init/Data/List/Erase.lean index 99d2a3e698..8cfa2ac8f8 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -12,8 +12,8 @@ import Init.Data.List.Find # Lemmas about `List.eraseP`, `List.erase`, and `List.eraseIdx`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/FinRange.lean b/src/Init/Data/List/FinRange.lean index 73d6bf843e..1aa26088fc 100644 --- a/src/Init/Data/List/FinRange.lean +++ b/src/Init/Data/List/FinRange.lean @@ -6,8 +6,8 @@ Authors: François G. Dorais prelude import Init.Data.List.OfFn --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Find.lean b/src/Init/Data/List/Find.lean index 9b0cd4bac3..59e43f877e 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -15,8 +15,8 @@ Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `L and `List.lookup`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Impl.lean b/src/Init/Data/List/Impl.lean index f608b83346..d494ed211a 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -16,8 +16,8 @@ If you import `Init.Data.List.Basic` but do not import this file, then at runtime you will get non-tail recursive versions of the following definitions. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 63b085e7a8..52428e8384 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -74,8 +74,8 @@ Also -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Lex.lean b/src/Init/Data/List/Lex.lean index a616986ac4..bf05b4255f 100644 --- a/src/Init/Data/List/Lex.lean +++ b/src/Init/Data/List/Lex.lean @@ -7,8 +7,8 @@ prelude import Init.Data.List.Lemmas import Init.Data.List.Nat.TakeDrop --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index e87475eb5a..863ca640bb 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -11,8 +11,8 @@ import Init.Data.List.OfFn import Init.Data.Fin.Lemmas import Init.Data.Option.Attach --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/MinMax.lean b/src/Init/Data/List/MinMax.lean index 3d2e98d8db..7bc8b09c46 100644 --- a/src/Init/Data/List/MinMax.lean +++ b/src/Init/Data/List/MinMax.lean @@ -10,8 +10,8 @@ import Init.Data.List.Lemmas # Lemmas about `List.min?` and `List.max?. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Monadic.lean b/src/Init/Data/List/Monadic.lean index f48e9908eb..e0e49acbc6 100644 --- a/src/Init/Data/List/Monadic.lean +++ b/src/Init/Data/List/Monadic.lean @@ -11,8 +11,8 @@ import Init.Data.List.Attach # Lemmas about `List.mapM` and `List.forM`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/BEq.lean b/src/Init/Data/List/Nat/BEq.lean index a486fb4db6..d592bb62bc 100644 --- a/src/Init/Data/List/Nat/BEq.lean +++ b/src/Init/Data/List/Nat/BEq.lean @@ -7,8 +7,8 @@ prelude import Init.Data.Nat.Lemmas import Init.Data.List.Basic --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index ba0977e870..ac02383dc8 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -15,8 +15,8 @@ import Init.Data.Nat.Lemmas In particular, `omega` is available here. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open Nat diff --git a/src/Init/Data/List/Nat/Count.lean b/src/Init/Data/List/Nat/Count.lean index 9fa6ebc96d..86c457156a 100644 --- a/src/Init/Data/List/Nat/Count.lean +++ b/src/Init/Data/List/Nat/Count.lean @@ -7,8 +7,8 @@ prelude import Init.Data.List.Count import Init.Data.Nat.Lemmas --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/Erase.lean b/src/Init/Data/List/Nat/Erase.lean index f62f79f1fe..7508a3a5dd 100644 --- a/src/Init/Data/List/Nat/Erase.lean +++ b/src/Init/Data/List/Nat/Erase.lean @@ -7,8 +7,8 @@ prelude import Init.Data.List.Nat.TakeDrop import Init.Data.List.Erase --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/Find.lean b/src/Init/Data/List/Nat/Find.lean index 4d2e0dce3f..7906de386f 100644 --- a/src/Init/Data/List/Nat/Find.lean +++ b/src/Init/Data/List/Nat/Find.lean @@ -7,8 +7,8 @@ prelude import Init.Data.List.Nat.Range import Init.Data.List.Find --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean index 4fd54205a9..26c8aa8582 100644 --- a/src/Init/Data/List/Nat/InsertIdx.lean +++ b/src/Init/Data/List/Nat/InsertIdx.lean @@ -12,8 +12,8 @@ import Init.Data.List.Nat.Modify Proves various lemmas about `List.insertIdx`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open Function Nat diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean index 9797582f98..8fe58713a0 100644 --- a/src/Init/Data/List/Nat/Modify.lean +++ b/src/Init/Data/List/Nat/Modify.lean @@ -8,8 +8,8 @@ prelude import Init.Data.List.Nat.TakeDrop import Init.Data.List.Nat.Erase --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/Pairwise.lean b/src/Init/Data/List/Nat/Pairwise.lean index a3cdfc1295..184ae03c74 100644 --- a/src/Init/Data/List/Nat/Pairwise.lean +++ b/src/Init/Data/List/Nat/Pairwise.lean @@ -12,8 +12,8 @@ import Init.Data.List.Pairwise # Lemmas about `List.Pairwise` -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/Perm.lean b/src/Init/Data/List/Nat/Perm.lean index 0e743dc62c..114b6d2243 100644 --- a/src/Init/Data/List/Nat/Perm.lean +++ b/src/Init/Data/List/Nat/Perm.lean @@ -7,8 +7,8 @@ prelude import Init.Data.List.Nat.TakeDrop import Init.Data.List.Perm --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean index c66b26a1fc..2111287ffc 100644 --- a/src/Init/Data/List/Nat/Range.lean +++ b/src/Init/Data/List/Nat/Range.lean @@ -14,8 +14,8 @@ import Init.Data.List.Erase # Lemmas about `List.range` and `List.enum` -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/Sublist.lean b/src/Init/Data/List/Nat/Sublist.lean index 8f3701ff1b..944f27cea7 100644 --- a/src/Init/Data/List/Nat/Sublist.lean +++ b/src/Init/Data/List/Nat/Sublist.lean @@ -16,8 +16,8 @@ These are in a separate file from most of the lemmas about `List.IsSuffix` as they required importing more lemmas about natural numbers, and use `omega`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index ede571ef92..0e76860817 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -16,8 +16,8 @@ These are in a separate file from most of the list lemmas as they required importing more lemmas about natural numbers, and use `omega`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace List @@ -115,12 +115,12 @@ theorem take_set_of_le (a : α) {i j : Nat} (l : List α) (h : j ≤ i) : @[deprecated take_set_of_le (since := "2025-02-04")] abbrev take_set_of_lt := @take_set_of_le -@[simp] theorem take_replicate (a : α) : ∀ i j : Nat, take i (replicate j a) = replicate (min i j) a +@[simp] theorem take_replicate (a : α) : ∀ i n : Nat, take i (replicate n a) = replicate (min i n) a | n, 0 => by simp [Nat.min_zero] | 0, m => by simp [Nat.zero_min] | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate] -@[simp] theorem drop_replicate (a : α) : ∀ i j : Nat, drop i (replicate j a) = replicate (j - i) a +@[simp] theorem drop_replicate (a : α) : ∀ i n : Nat, drop i (replicate n a) = replicate (n - i) a | n, 0 => by simp | 0, m => by simp | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate] diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean index d0c8729bbc..a213a220a3 100644 --- a/src/Init/Data/List/Notation.lean +++ b/src/Init/Data/List/Notation.lean @@ -11,8 +11,8 @@ import Init.Data.Nat.Div.Basic -/ set_option linter.missingDocs true -- keep it documented --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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 50757907a5..03fec62c62 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/src/Init/Data/List/OfFn.lean @@ -11,8 +11,8 @@ import Init.Data.Fin.Fold # Theorems about `List.ofFn` -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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 f038b50eba..54f6f0e847 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/src/Init/Data/List/Pairwise.lean @@ -11,8 +11,8 @@ import Init.Data.List.Attach # Lemmas about `List.Pairwise` and `List.Nodup`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Perm.lean b/src/Init/Data/List/Perm.lean index 02370261d8..ce19f27a3e 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -18,8 +18,8 @@ another. The notation `~` is used for permutation equivalence. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open Nat diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean index 2382c667dd..613d236f2c 100644 --- a/src/Init/Data/List/Range.lean +++ b/src/Init/Data/List/Range.lean @@ -14,8 +14,8 @@ Most of the results are deferred to `Data.Init.List.Nat.Range`, where more resul natural arithmetic are available. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace List @@ -74,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) : - ∀ {i j : Nat}, i < j → (range' s j step)[i]? = some (s + step * i) + ∀ {i n : Nat}, i < n → (range' s n 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] @@ -147,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 {i j : Nat} (h : i < j) : (range j)[i]? = some i := by +theorem getElem?_range {i n : Nat} (h : i < n) : (range n)[i]? = some i := by simp [range_eq_range', getElem?_range' _ _ h] -@[simp] theorem getElem_range {i : Nat} (j) (h : j < (range i).length) : (range i)[j] = j := by +@[simp] theorem getElem_range {n : Nat} (j) (h : j < (range n).length) : (range n)[j] = j := by simp [range_eq_range'] theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n) := by @@ -183,9 +183,9 @@ theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by theorem range_succ (n : Nat) : range (succ n) = range n ++ [n] := by simp only [range_eq_range', range'_1_concat, Nat.zero_add] -theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by +theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by rw [← range'_eq_map_range] - simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm + simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm theorem head?_range (n : Nat) : (range n).head? = if n = 0 then none else some 0 := by induction n with diff --git a/src/Init/Data/List/Sort/Basic.lean b/src/Init/Data/List/Sort/Basic.lean index d976515c3d..98106e5787 100644 --- a/src/Init/Data/List/Sort/Basic.lean +++ b/src/Init/Data/List/Sort/Basic.lean @@ -14,8 +14,8 @@ These definitions are intended for verification purposes, and are replaced at runtime by efficient versions in `Init.Data.List.Sort.Impl`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index 16e63257e7..d20177127c 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/src/Init/Data/List/Sort/Impl.lean @@ -31,8 +31,8 @@ as long as such improvements are carefully validated by benchmarking, they can be done without changing the theory, as long as a `@[csimp]` lemma is provided. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open List diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index 0f6c3126a6..a018b37838 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -21,8 +21,8 @@ import Init.Data.Bool -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Sublist.lean b/src/Init/Data/List/Sublist.lean index 349e5216e3..e8b03beef4 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -11,8 +11,8 @@ import Init.Data.List.TakeDrop # Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index ed9329d1f8..250513d706 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -10,8 +10,8 @@ import Init.Data.List.Lemmas # Lemmas about `List.take` and `List.drop`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/ToArray.lean b/src/Init/Data/List/ToArray.lean index 4aa771267f..478e681ba5 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -15,8 +15,8 @@ import Init.Data.Array.Lex.Basic We prefer to pull `List.toArray` outwards past `Array` operations. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/ToArrayImpl.lean b/src/Init/Data/List/ToArrayImpl.lean index 2c0b30140c..d40fea7236 100644 --- a/src/Init/Data/List/ToArrayImpl.lean +++ b/src/Init/Data/List/ToArrayImpl.lean @@ -6,8 +6,8 @@ Authors: Henrik Böving prelude import Init.Data.List.Basic --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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`. diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index f9ea4445ce..8ee4ab766a 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -11,8 +11,8 @@ import Init.Data.Function # Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables 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/Vector/Count.lean b/src/Init/Data/Vector/Count.lean index 498b29dab6..238d9c7b02 100644 --- a/src/Init/Data/Vector/Count.lean +++ b/src/Init/Data/Vector/Count.lean @@ -11,8 +11,8 @@ import Init.Data.Vector.Lemmas # Lemmas about `Vector.countP` and `Vector.count`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector @@ -101,6 +101,7 @@ theorem countP_set (p : α → Bool) (xs : Vector α n) (i : Nat) (a : α) (h : rcases xs with ⟨xs, rfl⟩ simp +set_option linter.listVariables false in -- This can probably be removed later. @[simp] theorem countP_flatten (xss : Vector (Vector α m) n) : countP p xss.flatten = (xss.map (countP p)).sum := by rcases xss with ⟨xss, rfl⟩ @@ -159,6 +160,7 @@ theorem count_le_count_push (a b : α) (xs : Vector α n) : count a xs ≤ count count a (xs ++ ys) = count a xs + count a ys := countP_append .. +set_option linter.listVariables false in -- This can probably be removed later. @[simp] theorem count_flatten (a : α) (xss : Vector (Vector α m) n) : count a xss.flatten = (xss.map (count a)).sum := by rcases xss with ⟨xss, rfl⟩ diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean index ef299c1f56..d99d07f4c7 100644 --- a/src/Init/Data/Vector/DecidableEq.lean +++ b/src/Init/Data/Vector/DecidableEq.lean @@ -7,8 +7,8 @@ prelude import Init.Data.Array.DecidableEq import Init.Data.Vector.Lemmas --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/Erase.lean b/src/Init/Data/Vector/Erase.lean index c01567c400..4eb7e9f976 100644 --- a/src/Init/Data/Vector/Erase.lean +++ b/src/Init/Data/Vector/Erase.lean @@ -11,8 +11,8 @@ import Init.Data.Array.Erase # Lemmas about `Vector.eraseIdx`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean index f6e3abcb51..88f70b9dd2 100644 --- a/src/Init/Data/Vector/Extract.lean +++ b/src/Init/Data/Vector/Extract.lean @@ -11,8 +11,8 @@ import Init.Data.Array.Extract # Lemmas about `Vector.extract` -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open Nat diff --git a/src/Init/Data/Vector/FinRange.lean b/src/Init/Data/Vector/FinRange.lean index 4fd253d439..bad5a55652 100644 --- a/src/Init/Data/Vector/FinRange.lean +++ b/src/Init/Data/Vector/FinRange.lean @@ -7,8 +7,8 @@ prelude import Init.Data.Array.FinRange import Init.Data.Vector.OfFn --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/InsertIdx.lean b/src/Init/Data/Vector/InsertIdx.lean index d21a97b5f6..d2008e5091 100644 --- a/src/Init/Data/Vector/InsertIdx.lean +++ b/src/Init/Data/Vector/InsertIdx.lean @@ -13,8 +13,8 @@ import Init.Data.Array.InsertIdx Proves various lemmas about `Vector.insertIdx`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. open Function Nat diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 8449f64c95..342e118051 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -12,6 +12,7 @@ import Init.Data.Array.Find ## Vectors Lemmas about `Vector α n` -/ + -- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. -- set_option linter.indexVariables true -- Enforce naming conventions for index variables. @@ -2369,8 +2370,8 @@ theorem back?_eq_some_iff {xs : Vector α n} {a : α} : @[simp] theorem back_append_of_neZero {xs : Vector α n} {ys : Vector α m} [NeZero m] : (xs ++ ys).back = ys.back := by - rcases xs with ⟨l⟩ - rcases ys with ⟨l'⟩ + rcases xs with ⟨xs, rfl⟩ + rcases ys with ⟨ys, rfl⟩ simp only [mk_append_mk, back_mk] rw [Array.back_append_of_size_pos] @@ -2416,6 +2417,7 @@ theorem back?_flatMap {xs : Vector α n} {f : α → Vector β m} : simp [Array.back?_flatMap] rfl +set_option linter.listVariables false in -- This can probably be removed later. theorem back?_flatten {xss : Vector (Vector α m) n} : (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by rcases xss with ⟨xss, rfl⟩ diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 79b6ef9058..655eb47d4e 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -8,8 +8,8 @@ import Init.Data.Vector.Basic import Init.Data.Vector.Lemmas import Init.Data.Array.Lex.Lemmas --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean index 3bb9cb8473..df7ab6ef59 100644 --- a/src/Init/Data/Vector/MapIdx.lean +++ b/src/Init/Data/Vector/MapIdx.lean @@ -8,8 +8,8 @@ import Init.Data.Array.MapIdx import Init.Data.Vector.Attach import Init.Data.Vector.Lemmas --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index 1304ccbcdf..438745abfb 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -13,8 +13,8 @@ import Init.Control.Lawful.Lemmas # Lemmas about `Vector.forIn'` and `Vector.forIn`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean index f776d5b786..27f2fd3806 100644 --- a/src/Init/Data/Vector/OfFn.lean +++ b/src/Init/Data/Vector/OfFn.lean @@ -11,8 +11,8 @@ import Init.Data.Array.OfFn # Theorems about `Vector.ofFn` -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean index 99c129a3e3..0d1ec0ea49 100644 --- a/src/Init/Data/Vector/Range.lean +++ b/src/Init/Data/Vector/Range.lean @@ -14,8 +14,8 @@ import Init.Data.Array.Range -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Init/Data/Vector/Zip.lean b/src/Init/Data/Vector/Zip.lean index ad420a8cb7..491b2c4cc8 100644 --- a/src/Init/Data/Vector/Zip.lean +++ b/src/Init/Data/Vector/Zip.lean @@ -11,8 +11,8 @@ import Init.Data.Vector.Lemmas # Lemmas about `Vector.zip`, `Vector.zipWith`, `Vector.zipWithAll`, and `Vector.unzip`. -/ --- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- set_option linter.indexVariables true -- Enforce naming conventions for index variables. +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +set_option linter.indexVariables true -- Enforce naming conventions for index variables. namespace Vector diff --git a/src/Lean/Linter/List.lean b/src/Lean/Linter/List.lean index ca723385c9..1ca61c9f3e 100644 --- a/src/Lean/Linter/List.lean +++ b/src/Lean/Linter/List.lean @@ -237,20 +237,23 @@ def listVariablesLinter : Linter if let .str _ n := n then let n := stripBinderName n if !allowedListNames.contains n then - unless (ty.getArg! 0).isAppOf `List && (n == "L" || n == "xss") do + -- Allow `L` or `xss` for `List (List α)` or `List (Array α)` + unless ((ty.getArg! 0).isAppOf `List || (ty.getArg! 0).isAppOf `Array) && (n == "L" || n == "xss") do Linter.logLint linter.listVariables stx m!"Forbidden variable appearing as a `List` name: {n}" for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do if let .str _ n := n then let n := stripBinderName n if !allowedArrayNames.contains n then - unless (ty.getArg! 0).isAppOf `Array && n == "xss" do + -- Allow `xss` for `Array (Array α)` or `Array (Vector α)` + unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do Linter.logLint linter.listVariables stx m!"Forbidden variable appearing as a `Array` name: {n}" for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do if let .str _ n := n then let n := stripBinderName n if !allowedVectorNames.contains n then + -- Allow `xss` for `Vector (Vector α)` unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do Linter.logLint linter.listVariables stx m!"Forbidden variable appearing as a `Vector` name: {n}"