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
Equations
- Lean.ForEachExprWhere.initCache = { visited := mkArray Lean.ForEachExprWhere.cacheSize.toNat (cast Lean.ForEachExprWhere.initCache.proof_1 ()), checked := ∅ }
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Expr.forEachWhere
(unsafe) implementation
Equations
- Lean.ForEachExprWhere.visit p f e stopWhenVisited = (Lean.ForEachExprWhere.visit.go p f stopWhenVisited e).run' Lean.ForEachExprWhere.initCache
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
e.forEachWhere p f
applies f
to each subterm that satisfies p
.
If stopWhenVisited
is true
, the function doesn't visit subterms of terms
which satisfy p
.