From c91a2c63c22ed4d381b21df2643765da73dfbabf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 11 Jan 2026 23:38:16 +0100 Subject: [PATCH] perf: fast paths for forEachWhere Expr.isFVar (#11973) Add a fast path for the pattern `forEachWhere Expr.isFVar` to avoid setting up the expression traversal etc. Pattern initially noticed by @Rob23oba --- src/Lean/Compiler/LCNF/Closure.lean | 3 ++- src/Lean/Meta/Tactic/Util.lean | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Closure.lean b/src/Lean/Compiler/LCNF/Closure.lean index c17c2f9c13..de77803a2c 100644 --- a/src/Lean/Compiler/LCNF/Closure.lean +++ b/src/Lean/Compiler/LCNF/Closure.lean @@ -156,7 +156,8 @@ mutual /-- Collect dependencies of the given expression. -/ partial def collectType (type : Expr) : ClosureM Unit := do - type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId! + if type.hasFVar then + type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId! end diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index e1fd8cc809..d085c40a6f 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -99,7 +99,8 @@ def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId let removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do let e ← instantiateMVars e let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do - e.forEachWhere Expr.isFVar fun e => modify fun s => s.erase e.fvarId! + if e.hasFVar then + e.forEachWhere Expr.isFVar fun e => modify fun s => s.erase e.fvarId! get visit |>.run' candidates mvarId.withContext do