Lean.Meta.Transform

Type

done: Lean.Expr → Lean.TransformStep
visit: Lean.Expr → 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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) :

m Lean.Expr

Tranform the expression input using pre and post.

pre s is invoked before visiting the children of subterm 's'. If the result is TransformStep.visit sNew, then sNew is traversed by transform. If the result is TransformStep.done sNew, then s is just replaced with sNew. In both cases, sNew must be definitionally equal to s
post s is invoked after visiting the children of subterm s.

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 _ := { }; let __1 := { monadLift := fun {α} x => liftM (liftM x) }; Lean.MonadCacheT.run (Lean.Core.transform.visit pre post _ __1 input)

source

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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (_ : STWorld IO.RealWorld m) (_ : MonadLiftT (ST IO.RealWorld) m) (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (_ : STWorld IO.RealWorld m) (_ : MonadLiftT (ST IO.RealWorld) m) (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

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

Lean.CoreM Lean.Expr

Equations

Lean.Core.betaReduce e = Lean.Core.transform e (fun e => pure (Lean.TransformStep.visit (Lean.Expr.headBeta e))) fun e => pure (Lean.TransformStep.done e)

source

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 e => pure (Lean.TransformStep.visit e)) (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.

source

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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (usedLetOnly : optParam Bool false) (_ : STWorld IO.RealWorld m) (_ : MonadLiftT (ST IO.RealWorld) m) (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (usedLetOnly : optParam Bool false) (_ : STWorld IO.RealWorld m) (_ : MonadLiftT (ST IO.RealWorld) m) (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (usedLetOnly : optParam Bool false) (_ : STWorld IO.RealWorld m) (_ : MonadLiftT (ST IO.RealWorld) m) (fvars : Array Lean.Expr) (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (usedLetOnly : optParam Bool false) (_ : STWorld IO.RealWorld m) (_ : MonadLiftT (ST IO.RealWorld) m) (fvars : Array Lean.Expr) (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

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 e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) (usedLetOnly : optParam Bool false) (_ : STWorld IO.RealWorld m) (_ : MonadLiftT (ST IO.RealWorld) m) (fvars : Array Lean.Expr) (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

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

Lean.MetaM Lean.Expr

Equations

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

source

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.

source

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

Lean.CoreM Lean.Expr

Equations

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

source

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

Lean.CoreM Lean.Expr

Equations

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