inductive Lean.TransformStep : Type

• done (e : Expr) : TransformStep

  Return expression without visiting any subexpressions.

• visit (e : Expr) : TransformStep

  Visit expression (which should be different from current expression) instead. The new expression e is passed to pre again.

• continue (e? : Option Expr := none) : TransformStep

  Continue transformation with the given expression (defaults to current expression). For pre, this means visiting the children of the expression. For post, this is equivalent to returning done.

instance Lean.instInhabitedTransformStep : Inhabited TransformStep

Equations

• Lean.instInhabitedTransformStep = { default := Lean.TransformStep.done default }

instance Lean.instReprTransformStep : Repr TransformStep

Equations

• Lean.instReprTransformStep = { reprPrec := Lean.reprTransformStep✝ }

def Lean.Core.transform {m : Type → Type} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m] (input : Expr) (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) : m Expr

Transform the expression input using pre and post.

• First pre is invoked with the current expression and recursion is continued according to the TransformStep result. In all cases, the expression contained in the result, if any, must be definitionally equal to the current expression.
• After recursion, if any, post is invoked on the resulting expression.

The term s in both pre s and post s may contain loose bound variables. So, this method is not appropriate for if one needs to apply operations (e.g., whnf, inferType) that do not handle loose bound variables. Consider using Meta.transform to avoid loose bound variables.

This method is useful for applying transformations such as beta-reduction and delta-reduction.

Equations

• Lean.Core.transform input pre post = (Lean.Core.transform.visit pre post { } { monadLift := fun {α : Type} (x : ST IO.RealWorld α) => liftM (liftM x) } input).run

partial def Lean.Core.transform.visit {m : Type → Type} [Monad m] [MonadControlT CoreM m] (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (e : Expr) → MonadCacheT ExprStructEq Expr m Expr

partial def Lean.Core.transform.visit.visitPost {m : Type → Type} [Monad m] [MonadControlT CoreM m] (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (e : Expr) → MonadCacheT ExprStructEq Expr m Expr

def Lean.Core.betaReduce (e : Expr) : CoreM Expr

Equations

• Lean.Core.betaReduce e = Lean.Core.transform e fun (e : Lean.Expr) => pure (if e.isHeadBetaTarget = true then Lean.TransformStep.visit e.headBeta else Lean.TransformStep.continue)

@[inline]

def Lean.Meta.transformWithCache {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (input : Expr) (cache : Std.HashMap ExprStructEq Expr) (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (usedLetOnly skipConstInApp : Bool := false) : m (Expr × Std.HashMap ExprStructEq Expr)

Similar to Meta.transform, but allows the use of a pre-existing cache.

Warnings:

• For the cache to be valid, it must always use the same pre and post functions.
• It is important that there are no other references to cache when it is passed to transformWithCache, to avoid unnecessary copying of the hash map.

Equations

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

partial def Lean.Meta.transformWithCache.visit {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (usedLetOnly skipConstInApp : Bool := false) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (e : Expr) → MonadCacheT ExprStructEq Expr m Expr

partial def Lean.Meta.transformWithCache.visit.visitPost {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (usedLetOnly skipConstInApp : Bool := false) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (e : Expr) → MonadCacheT ExprStructEq Expr m Expr

partial def Lean.Meta.transformWithCache.visit.visitLambda {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (usedLetOnly skipConstInApp : Bool := false) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (fvars : Array Expr) → (e : Expr) → MonadCacheT ExprStructEq Expr m Expr

partial def Lean.Meta.transformWithCache.visit.visitForall {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (usedLetOnly skipConstInApp : Bool := false) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (fvars : Array Expr) → (e : Expr) → MonadCacheT ExprStructEq Expr m Expr

partial def Lean.Meta.transformWithCache.visit.visitLet {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (usedLetOnly skipConstInApp : Bool := false) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (fvars : Array Expr) → (e : Expr) → MonadCacheT ExprStructEq Expr m Expr

def Lean.Meta.transform {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (input : Expr) (pre : Expr → m TransformStep := fun (x : Expr) => pure TransformStep.continue) (post : Expr → m TransformStep := fun (e : Expr) => pure (TransformStep.done e)) (usedLetOnly skipConstInApp : Bool := false) : m Expr

Similar to Core.transform, but terms provided to pre and post do not contain loose bound variables. So, it is safe to use any MetaM method at pre and post.

Warning: pre and post should not depend on variables in the local context introduced by transform. This is in order to allow aggressive caching.

If skipConstInApp := true, then for an expression mkAppN (.const f) args, the subexpression .const f is not visited again. Put differently: every .const f is visited once, with its arguments if present, on its own otherwise.

Equations

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

def Lean.Meta.zetaReduce (e : Expr) : MetaM Expr

Equations

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

def Lean.Meta.zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr

Zeta reduces only the provided fvars, beta reducing the substitutions.

Equations

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

def Lean.Meta.unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr

Unfold definitions and theorems in e that are not in the current environment, but are in biggerEnv.

Equations

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

def Lean.Meta.eraseInaccessibleAnnotations (e : Expr) : CoreM Expr

Equations

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

def Lean.Meta.erasePatternRefAnnotations (e : Expr) : CoreM Expr

Equations

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