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 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
      @[reducible, inline]
      abbrev Lean.ForEachExprWhere.ForEachM {ω : Type} (m : TypeType) [STWorld ω m] (α : Type) :
      Equations
      Instances For
        Instances For
          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 : Lean.ExprBool) (f : Lean.Exprm Unit) (e : Lean.Expr) (stopWhenVisited : optParam Bool false) :

            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) (stopWhenVisited : optParam Bool false) (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) (stopWhenVisited : optParam 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.