From 30d625697e13bb23b6ad02aa49d16fe55fbe4bb7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Nov 2022 18:44:20 -0800 Subject: [PATCH] chore: use `Expr.forEachWhere` to implement linter closes #1899 TODO: use `Expr.forEachWhere` in other modules. There are many other opportunities. --- src/Lean/Linter/UnusedVariables.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index cad32754e7..1aaf666c60 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/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 @@ -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