From 60c8a722623ce0393bc74560c25de3a3327ee4bc Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Sat, 4 Jun 2022 23:28:47 +0200
Subject: [PATCH] fix: unused variables linter: consider induction variables as
 pattern variables

---
 src/Lean/Linter/Basic.lean                    |  4 +++-
 tests/lean/linterUnusedVariables.lean         |  8 +++++++
 .../linterUnusedVariables.lean.expected.out   | 21 ++++++++++---------
 3 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index 83cada6aa9..15884e3aca 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -186,7 +186,9 @@ where
     stackMatches stack [`null, `Lean.Parser.Term.paren, `null, `Lean.Parser.Term.basicFun]
 
   isPatternVar (_ : Syntax) (stack : SyntaxStack) :=
-    stack.any fun (stx, pos) => stx.isOfKind `Lean.Parser.Term.matchAlt && pos == 1
+    stack.any fun (stx, pos) =>
+      (stx.isOfKind `Lean.Parser.Term.matchAlt && pos == 1) ||
+      (stx.isOfKind `Lean.Parser.Tactic.inductionAlt && pos == 2)
 
 builtin_initialize addLinter unusedVariables
 
diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
index 64965d2fbd..3e677c2979 100644
--- a/tests/lean/linterUnusedVariables.lean
+++ b/tests/lean/linterUnusedVariables.lean
@@ -124,6 +124,14 @@ def nolintPatternVars (x : Option (Option Nat)) : Nat :=
   | some (some y) => (fun z => 1) 2
   | _ => 0
 
+set_option linter.unusedVariables.patternVars false in
+theorem nolintPatternVarsInduction (n : Nat) : True := by
+  induction n with
+  | zero => exact True.intro
+  | succ m =>
+    have h : True := by simp
+    exact True.intro
+
 
 inductive Foo (α : Type)
   | foo (x : Nat) (y : Nat)
diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
index b1f8d29a57..d71e3f4bf9 100644
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -16,13 +16,14 @@ linterUnusedVariables.lean:107:25-107:26: warning: unused variable `x`
 linterUnusedVariables.lean:108:6-108:7: warning: unused variable `y`
 linterUnusedVariables.lean:114:6-114:7: warning: unused variable `a`
 linterUnusedVariables.lean:124:26-124:27: warning: unused variable `z`
-linterUnusedVariables.lean:138:8-138:9: warning: unused variable `y`
-linterUnusedVariables.lean:142:7-142:8: warning: unused variable `x`
-linterUnusedVariables.lean:141:20-141:21: warning: unused variable `β`
-linterUnusedVariables.lean:152:6-152:7: warning: unused variable `s`
-linterUnusedVariables.lean:159:13-159:14: warning: unused variable `s`
-linterUnusedVariables.lean:176:6-176:7: warning: unused variable `y`
-linterUnusedVariables.lean:183:19-183:20: warning: unused variable `x`
-linterUnusedVariables.lean:187:6-187:7: warning: unused variable `y`
-linterUnusedVariables.lean:192:6-192:7: warning: unused variable `y`
-linterUnusedVariables.lean:197:6-197:7: warning: unused variable `y`
+linterUnusedVariables.lean:132:9-132:10: warning: unused variable `h`
+linterUnusedVariables.lean:146:8-146:9: warning: unused variable `y`
+linterUnusedVariables.lean:150:7-150:8: warning: unused variable `x`
+linterUnusedVariables.lean:149:20-149:21: warning: unused variable `β`
+linterUnusedVariables.lean:160:6-160:7: warning: unused variable `s`
+linterUnusedVariables.lean:167:13-167:14: warning: unused variable `s`
+linterUnusedVariables.lean:184:6-184:7: warning: unused variable `y`
+linterUnusedVariables.lean:191:19-191:20: warning: unused variable `x`
+linterUnusedVariables.lean:195:6-195:7: warning: unused variable `y`
+linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y`
+linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`