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

fix: ignore unused anonymous have variables

Browse source
This commit is contained in:
Mario Carneiro 2022-09-18 17:00:15 -04:00 • committed by Sebastian Ullrich
parent 6bf01ebd30
commit 2270e8cd53
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Linter/UnusedVariables.lean
View file

@ -102,6 +102,11 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
(stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
(stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2))
-- is anonymous have variable
builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun stx stack _ =>
stx.getId == `this &&
(stack.matches [none, ``Lean.Parser.Term.haveIdDecl] ||
stack.matches [none, ``Lean.Parser.Term.haveEqnsDecl]))
builtin_initialize unusedVariablesIgnoreFnsExt : SimplePersistentEnvExtension Name Unit ←
registerSimplePersistentEnvExtension {