# Documentation

## Lean.Meta.ForEachExpr

def Lean.Meta.visitLambda {m : TypeType u_1} [] (f : ) (e : Lean.Expr) :

Given an expression e = fun (x₁ : α₁) .. (xₙ : αₙ) => b, runs f on each αᵢ and b.

Equations
Instances For
def Lean.Meta.visitLambda.visit {m : TypeType u_1} [] (f : ) (fvars : ) :
Equations
Instances For
def Lean.Meta.visitForall {m : TypeType u_1} [] (f : ) (e : Lean.Expr) :

Given an expression e = (x₁ : α₁) → .. (xₙ : αₙ) → b, runs f on each αᵢ and b.

Equations
Instances For
def Lean.Meta.visitForall.visit {m : TypeType u_1} [] (f : ) (fvars : ) :
Equations
Instances For
def Lean.Meta.visitLet {m : TypeType u_1} [] (f : ) (e : Lean.Expr) :

Given a sequence of let binders let (x₁ : α₁ := v₁) ... in b, runs f on each αᵢ, vᵢ and b.

Equations
Instances For
def Lean.Meta.visitLet.visit {m : TypeType u_1} [] (f : ) (fvars : ) :
Equations
Instances For
def Lean.Meta.forEachExpr' {m : } [] [] (input : Lean.Expr) (fn : ) :

Similar to Expr.forEach', but creates free variables whenever going inside of a binder. If the inner function returns false, deeper subexpressions will not be visited.

Equations
Instances For
partial def Lean.Meta.forEachExpr'.visit {m : } [] (fn : ) :
(x : ) →
def Lean.Meta.forEachExpr {m : } [] [] (e : Lean.Expr) (f : ) :

Similar to Expr.forEach, but creates free variables whenever going inside of a binder.

Equations
Instances For
def Lean.Meta.setMVarUserNamesAt (e : Lean.Expr) (isTarget : ) :

Auxiliary method for (temporarily) setting the user facing name of metavariables. Let ?m be a metavariable in isTarget.contains ?m, and ?m does not have a user facing name. Then, we try to find an application f ... ?m in e, and (temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for ?m. This method returns all metavariables whose user facing name has been updated.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.resetMVarUserNames (toReset : ) :

Remove user facing name for metavariables in toReset. This a low-level method for "undoing" the effect of setMVarUserNamesAt

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.mkForallFVars' (xs : ) (type : Lean.Expr) :

Similar to mkForallFVars, but tries to infer better binder names when xs contains metavariables. Let ?m be a metavariable in xs s.t. ?m does not have a user facing name. Then, we try to find an application f ... ?m in the other binder typer and type, and (temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for ?m. The "renaming" is temporary.

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