Skip to content

Commit

Permalink
chore: use Expr.forEachWhere to implement linter
Browse files Browse the repository at this point in the history
closes leanprover#1899

TODO: use `Expr.forEachWhere` in other modules. There are many other opportunities.
  • Loading branch information
leodemoura committed Dec 1, 2022
1 parent 1c5706b commit 30d6256
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/Lean/Linter/UnusedVariables.lean
@@ -1,4 +1,5 @@
import Lean.Elab.Command
import Lean.Util.ForEachExprWhere
import Lean.Linter.Util
import Lean.Server.References

Expand Down Expand Up @@ -179,9 +180,7 @@ def unusedVariables : Linter := fun cmdStx => do

let tacticFVarUses : HashSet FVarId ←
tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do
let (_, s) ← StateT.run (s := uses) <| expr.forEach fun
| .fvar id => modify (·.insert id)
| _ => pure ()
let (_, s) ← StateT.run (s := uses) <| expr.forEachWhere Expr.isFVar fun e => modify (·.insert e.fvarId!)
return s

-- collect ignore functions
Expand Down

0 comments on commit 30d6256

Please sign in to comment.