max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: unused variables linter: consider induction variables as pattern variables

Browse source
This commit is contained in:
larsk21 2022-06-04 23:28:47 +02:00 • committed by Leonardo de Moura
parent a9293410a2
commit 60c8a72262
3 changed files with 22 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Linter/Basic.lean
View file

@ -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

8
tests/lean/linterUnusedVariables.lean
View file

@ -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)

21
tests/lean/linterUnusedVariables.lean.expected.out
View file

@ -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`