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.

def Lean.instInhabitedTransformStep.default : TransformStep

Equations

• Lean.instInhabitedTransformStep.default = Lean.TransformStep.done default

@[implicit_reducible]

instance Lean.instInhabitedTransformStep : Inhabited TransformStep

Equations

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

@[implicit_reducible]

instance Lean.instReprTransformStep : Repr TransformStep

Equations

• Lean.instReprTransformStep = { reprPrec := Lean.instReprTransformStep.repr }

def Lean.instReprTransformStep.repr : TransformStep → Nat → Format

Equations

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

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

Recursively transforms input using pre and post callbacks.

For each subexpression:

1. pre is invoked first; recursion continues according to the TransformStep result.
2. After recursion (if any), post is invoked on the resulting expression.

The expressions passed to pre and post may contain loose bound variables. Use Meta.transform instead if you need operations like whnf or inferType that require expressions without loose bound variables.

Results are cached using pointer equality (ExprStructEq), so structurally identical subexpressions are transformed only once.

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

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

Applies beta reduction to all beta-reducible subexpressions in e.

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 skipInstances : Bool := false) : m (Expr × Std.HashMap ExprStructEq Expr)

Like Meta.transform, but accepts and returns a cache for reuse across multiple calls.

Parameters:

• usedLetOnly: when true, mkLambdaFVars/mkForallFVars/mkLetFVars only abstract over variables that are actually used in the body.
• skipConstInApp: when true, constant heads in applications are not visited separately.
• skipInstances: when true, instance arguments (determined via getFunInfo) are not visited.

The skipInstances flag is used by dsimp to avoid rewriting instances.

Warnings:

• The cache is only valid when using the same pre and post functions.
• Ensure there are no other references to cache to avoid unnecessary hash map copying.

Equations

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

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

Replaces all free variables in e that have let-values with their values. The substitution is applied recursively to the values themselves.

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 specified free variables, applying beta reduction after substitution. For example, if x has value fun y => y + 1 and appears as x 2, the result is 2 + 1.

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.unfoldIfArgIsAppOf (fnNames : Array Name) (numSectionVars : Nat) (e : Expr) : CoreM Expr

Unfolds theorems that are applied to f x₁ .. xₙ where f is in fnNames and n ≤ numSectionVars (i.e., an unsaturated application of f).

This is used to undo proof abstraction for termination checking, as otherwise the bare occurrence of the recursive function prevents termination checking from succeeding.

Usually, the argument is just f (the constant), arising from mkAuxTheorem abstracting over the aux decl representing f. If the mutual function is defined within the scope of variable commands, it is f x y where x y are the variables in scope, so we use the numSectionVars to recognize that while avoiding to unfold theorems applied to saturated applications of f.

This unfolds from the private environment. The resulting definitions are (usually) not exposed anyways.

Equations

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

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

Removes all inaccessible annotations from e.

Equations

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

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

Removes all patternWithRef annotations from e.

Equations

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