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.

@[reducible, inline]
Equations
Instances For
    • 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.

    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible, inline]
        abbrev Lean.ForEachExprWhere.ForEachM {ω : Type} (m : TypeType) [STWorld ω m] (α : Type) :
        Equations
        Instances For
          unsafe def Lean.ForEachExprWhere.visited {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Expr) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.ForEachExprWhere.checked {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Expr) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              unsafe def Lean.ForEachExprWhere.visit {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (p : ExprBool) (f : Exprm Unit) (e : Expr) (stopWhenVisited : Bool := false) :

              Expr.forEachWhere (unsafe) implementation

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

                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.