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

perf: reduce allocations in unused variable linter

Browse source
This commit is contained in:
Henrik 2023-08-31 03:41:10 +02:00 • committed by Sebastian Ullrich
parent ba416f2c1c
commit 0d5f9122a1
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,5 +1,5 @@
import Lean.Elab.Command
import Lean.Util.ForEachExprWhere
import Lean.Util.ForEachExpr
import Lean.Linter.Util
import Lean.Server.References
@ -181,7 +181,7 @@ def unusedVariables : Linter where
let tacticFVarUses : HashSet FVarId ←
tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do
let (_, s) ← StateT.run (s := uses) <| expr.forEachWhere Expr.isFVar fun e => modify (·.insert e.fvarId!)
let (_, s) ← StateT.run (s := uses) <| expr.forEach fun e => do if e.isFVar then modify (·.insert e.fvarId!)
return s
-- collect ignore functions