forEachWhere p f e
is similar to forEach f e
, but only applies f
to subterms that satisfy the
(pure) predicate p
.
It also uses the caching trick used at FindExpr
and ReplaceExpr
. This can be very effective
if the number of subterms satisfying p
is a small subset of the set of subterms.
If p
holds for most subterms, then it is more efficient to use forEach f e
.
Implements caching trick similar to the one used at
FindExpr
andReplaceExpr
.- checked : Lean.HashSet Lean.Expr
Set of visited subterms that satisfy the predicate
p
. We have to use this set to make suref
is applied at most once of each subterm that satisfiesp
.
Instances For
unsafe def
Lean.ForEachExprWhere.visited
{ω : Type}
{m : Type → Type}
[STWorld ω m]
[MonadLiftT (ST ω) m]
[Monad m]
(e : Lean.Expr)
:
Instances For
def
Lean.ForEachExprWhere.checked
{ω : Type}
{m : Type → Type}
[STWorld ω m]
[MonadLiftT (ST ω) m]
[Monad m]
(e : Lean.Expr)
: