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]
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
      @[inline, reducible]
      abbrev Lean.ForEachExprWhere.ForEachM {ω : Type} (m : TypeType) [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (α : Type) :
      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
            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

            Equations
            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) :
              Equations
              • One or more equations did not get rendered due to their size.
              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.