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

fix: support new inductionAlt syntax at Linter/Basic.lean

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-14 11:31:26 -07:00
parent bd2cccf287
commit 3a1dc5e066
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -195,7 +195,7 @@ where
isPatternVar (_ : Syntax) (stack : SyntaxStack) :=
stack.any fun (stx, pos) =>
(stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
(stx.isOfKind ``Lean.Parser.Tactic.inductionAlt && pos == 2)
(stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2)
builtin_initialize addLinter unusedVariables