Documentation

Lean.Meta.ForEachExpr

source
@[inline]
abbrev Lean.Meta.ForEachExpr.M (α : Type) :
Type
Equations
source
partial def Lean.Meta.ForEachExpr.visit (fn : Lean.Expr → Lean.MetaM Bool) (e : Lean.Expr) :
Lean.Meta.ForEachExpr.M Unit
source
def Lean.Meta.forEachExpr' (e : Lean.Expr) (f : Lean.Expr → Lean.MetaM Bool) :
Lean.MetaM Unit

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

Equations
source
def Lean.Meta.forEachExpr (e : Lean.Expr) (f : Lean.Expr → Lean.MetaM Unit) :
Lean.MetaM Unit

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

Equations
source
def Lean.Meta.setMVarUserNamesAt (e : Lean.Expr) (isTarget : Array Lean.Expr) :
Lean.MetaM (Array Lean.MVarId)

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.
source
def Lean.Meta.resetMVarUserNames (toReset : Array Lean.MVarId) :
Lean.MetaM Unit

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.
source
def Lean.Meta.mkForallFVars' (xs : Array Lean.Expr) (type : Lean.Expr) :
Lean.MetaM 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.