Documentation

Lean.Util.ForEachExprWhere

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.

@[inline, reducible]
Instances For
    • visited : Array Lean.Expr

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

    • 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.

    Instances For
      @[inline, reducible]
      abbrev Lean.ForEachExprWhere.ForEachM {ω : Type} (m : TypeType) [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (α : Type) :
      Instances For
        Instances For
          unsafe def Lean.ForEachExprWhere.visit {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Lean.ExprBool) (f : Lean.Exprm Unit) (e : Lean.Expr) :

          Expr.forEachWhere (unsafe) implementation

          Instances For
            unsafe def Lean.ForEachExprWhere.visit.go {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Lean.ExprBool) (f : Lean.Exprm Unit) (e : Lean.Expr) :
            Instances For
              @[implemented_by Lean.ForEachExprWhere.visit]
              opaque Lean.Expr.forEachWhere {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : Lean.ExprBool) (f : Lean.Exprm Unit) (e : Lean.Expr) :

              e.forEachWhere p f applies f to each subterm that satisfies p.