def Lean.Meta.visitLambda {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] (f : Expr → m Unit) (e : Expr) : m Unit

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

def Lean.Meta.visitLambda.visit {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] (f : Expr → m Unit) (fvars : Array Expr) : Expr → m Unit

def Lean.Meta.visitForall {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] (f : Expr → m Unit) (e : Expr) : m Unit

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

def Lean.Meta.visitForall.visit {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] (f : Expr → m Unit) (fvars : Array Expr) : Expr → m Unit

def Lean.Meta.visitLet {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] (f : Expr → m Unit) (e : Expr) : m Unit

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

def Lean.Meta.visitLet.visit {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] (f : Expr → m Unit) (fvars : Array Expr) : Expr → m Unit

def Lean.Meta.forEachExpr' {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (input : Expr) (fn : Expr → m Bool) : m Unit

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.

partial def Lean.Meta.forEachExpr'.visit {m : Type → Type} [Monad m] [MonadControlT MetaM m] (fn : Expr → m Bool) (x✝ : STWorld IO.RealWorld m) : MonadLiftT (ST IO.RealWorld) m → (e : Expr) → MonadCacheT Expr Unit m Unit

def Lean.Meta.forEachExpr {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (e : Expr) (f : Expr → m Unit) : m Unit

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

def Lean.Meta.setMVarUserNamesAt (e : Expr) (isTarget : Array Expr) : MetaM (Array 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.

def Lean.Meta.resetMVarUserNames (toReset : Array MVarId) : MetaM Unit

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

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