inductive Lean.TransformStep : Type

• Return expression without visiting any subexpressions.

  done: Lean.Expr → Lean.TransformStep

• Visit expression (which should be different from current expression) instead.

  visit: Lean.Expr → Lean.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.

  continue: optParam (Option Lean.Expr) none → Lean.TransformStep

def Lean.Core.transform {m : Type → Type} [inst : Monad m] [inst : MonadLiftT Lean.CoreM m] [inst : MonadControlT Lean.CoreM m] (input : Lean.Expr) (pre : optParam (Lean.Expr → m Lean.TransformStep) fun x => pure Lean.TransformStep.continue) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) : m Lean.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 = let x := { }; let x_1 := { monadLift := fun {α} x => liftM (liftM x) }; Lean.MonadCacheT.run (Lean.Core.transform.visit pre post x x_1 input)

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

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

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

Equations

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

def Lean.Meta.transform {m : Type → Type} [inst : Monad m] [inst : MonadLiftT Lean.MetaM m] [inst : MonadControlT Lean.MetaM m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] (input : Lean.Expr) (pre : optParam (Lean.Expr → m Lean.TransformStep) fun x => pure Lean.TransformStep.continue) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (usedLetOnly : optParam Bool false) : m Lean.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.

Equations

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

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

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

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

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

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

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

Equations

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

def Lean.Meta.unfoldDeclsFrom (biggerEnv : Lean.Environment) (e : Lean.Expr) : Lean.CoreM Lean.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 : Lean.Expr) : Lean.CoreM Lean.Expr

Equations

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

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

Equations

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