chore: fix linter.listVariables naming

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

@@ -8,7 +8,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array

src/Init/Data/List/Monadic.lean

@@ -11,7 +11,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List

src/Init/Data/List/Notation.lean

@@ -11,7 +11,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Decidable List

src/Init/Data/List/OfFn.lean

@@ -11,7 +11,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List

src/Init/Data/List/Pairwise.lean

@@ -11,7 +11,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List

src/Init/Data/List/Perm.lean

@@ -18,7 +18,7 @@ another.
 The notation `~` is used for permutation equivalence.
 -/
 
--- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` 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

src/Init/Data/List/Range.lean

@@ -14,7 +14,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List

src/Init/Data/List/Sublist.lean

@@ -11,7 +11,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List

src/Init/Data/List/TakeDrop.lean

@@ -10,7 +10,7 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.take` and `List.drop`.
 -/
 
--- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` 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

src/Init/Data/List/ToArray.lean

@@ -15,7 +15,7 @@ import Init.Data.Array.Lex.Basic
 We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
 
--- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` 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

src/Init/Data/List/ToArrayImpl.lean

@@ -6,7 +6,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 /--

src/Init/Data/List/Zip.lean

@@ -11,7 +11,7 @@ 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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List

src/Lean/Linter/List.lean

@@ -27,10 +27,10 @@ register_builtin_option linter.indexVariables : Bool := {
 }
 
 /--
-`set_option linter.listVariable true` enables a strict linter that
+`set_option linter.listVariables true` enables a strict linter that
 validates that all `List`/`Array`/`Vector` variables use standardized names.
 -/
-register_builtin_option linter.listVariable : Bool := {
+register_builtin_option linter.listVariables : Bool := {
   defValue := false
   descr := "Validate that all `List`/`Array`/`Vector` variables use allowed names."
 }
@@ -125,9 +125,9 @@ 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 listVariableLinter : Linter
+def listVariablesLinter : Linter
   where run := withSetOptionIn fun stx => do
-    unless (← getOptions).get linter.listVariable.name false do return
+    unless (← getOptions).get linter.listVariables.name false do return
     if (← get).messages.hasErrors then return
     if ! (← getInfoState).enabled then return
     for t in ← getInfoTrees do
@@ -138,21 +138,21 @@ def listVariableLinter : Linter
           let n := stripBinderName n
           if !allowedListNames.contains n then
             unless (ty.getArg! 0).isAppOf `List && n == "L" do
-              Linter.logLint linter.listVariable stx
+              Linter.logLint linter.listVariables 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.listVariable stx
+            Linter.logLint linter.listVariables 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.listVariable stx
+            Linter.logLint linter.listVariables stx
               m!"Forbidden variable appearing as a `Vector` name: {n}"
 
-builtin_initialize addLinter listVariableLinter
+builtin_initialize addLinter listVariablesLinter
 
 end Lean.Linter.List

tests/lean/run/list_name_linter.lean

@@ -1,4 +1,4 @@
-set_option linter.listVariable true
+set_option linter.listVariables true
 
 #guard_msgs in
 example (l : List Nat) : l = l := rfl
@@ -14,10 +14,10 @@ example (l₂ : List Nat) : l₂ = l₂ := rfl
 
 /--
 warning: Forbidden variable appearing as a `List` name: l₄
-note: this linter can be disabled with `set_option linter.listVariable false`
+note: this linter can be disabled with `set_option linter.listVariables false`
 ---
 warning: Forbidden variable appearing as a `List` name: l₄
-note: this linter can be disabled with `set_option linter.listVariable false`
+note: this linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (l₄ : List Nat) : l₄ = l₄ := rfl
@@ -27,20 +27,20 @@ example (xs : List Nat) : xs = xs := rfl
 
 /--
 warning: Forbidden variable appearing as a `List` name: ps
-note: this linter can be disabled with `set_option linter.listVariable false`
+note: this linter can be disabled with `set_option linter.listVariables false`
 ---
 warning: Forbidden variable appearing as a `List` name: ps
-note: this linter can be disabled with `set_option linter.listVariable false`
+note: this linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (ps : List Nat) : ps = ps := rfl
 
 /--
 warning: Forbidden variable appearing as a `Array` name: l
-note: this linter can be disabled with `set_option linter.listVariable false`
+note: this linter can be disabled with `set_option linter.listVariables false`
 ---
 warning: Forbidden variable appearing as a `Array` name: l
-note: this linter can be disabled with `set_option linter.listVariable false`
+note: this linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (l : Array Nat) : l = l := rfl