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.

@[reducible, inline]

abbrev Lean.ForEachExprWhere.cacheSize : USize

Equations

• Lean.ForEachExprWhere.cacheSize = 8192 - 1

structure Lean.ForEachExprWhere.State : Type

• visited : Array Expr

  Implements caching trick similar to the one used at FindExpr and ReplaceExpr.

• checked : Std.HashSet Expr

  Set of visited subterms that satisfy the predicate p. We have to use this set to make sure f is applied at most once of each subterm that satisfies p.

unsafe def Lean.ForEachExprWhere.initCache : State

Equations

• Lean.ForEachExprWhere.initCache = { visited := Array.replicate Lean.ForEachExprWhere.cacheSize.toNat (cast Lean.ForEachExprWhere.initCache._proof_1 ()), checked := ∅ }

@[reducible, inline]

abbrev Lean.ForEachExprWhere.ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] (α : Type) : Type

Equations

• Lean.ForEachExprWhere.ForEachM m = StateRefT' ω Lean.ForEachExprWhere.State m

unsafe def Lean.ForEachExprWhere.visited {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Expr) : ForEachM m Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.ForEachExprWhere.checked {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Expr) : ForEachM m Bool

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.ForEachExprWhere.visit {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Expr → Bool) (f : Expr → m Unit) (e : Expr) (stopWhenVisited : Bool := false) : m Unit

Expr.forEachWhere (unsafe) implementation

Equations

• Lean.ForEachExprWhere.visit p f e stopWhenVisited = (Lean.ForEachExprWhere.visit.go p f stopWhenVisited e).run' Lean.ForEachExprWhere.initCache

unsafe def Lean.ForEachExprWhere.visit.go {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Expr → Bool) (f : Expr → m Unit) (stopWhenVisited : Bool := false) (e : Expr) : StateRefT' ω State m Unit

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by Lean.ForEachExprWhere.visit]

opaque Lean.Expr.forEachWhere {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Expr → Bool) (f : Expr → m Unit) (e : Expr) (stopWhenVisited : Bool := false) : m Unit

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.