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

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

Equations

• Lean.Meta.visitLambda f e = Lean.Meta.visitLambda.visit f #[] e

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.visitLambda.visit f fvars x = f (Lean.Expr.instantiateRev x fvars)

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

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

Equations

• Lean.Meta.visitForall f e = Lean.Meta.visitForall.visit f #[] e

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.visitForall.visit f fvars x = f (Lean.Expr.instantiateRev x fvars)

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

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

Equations

• Lean.Meta.visitLet f e = Lean.Meta.visitLet.visit f #[] e

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.visitLet.visit f fvars x = f (Lean.Expr.instantiateRev x fvars)

def Lean.Meta.forEachExpr' {m : Type → Type} [inst : Monad m] [inst : MonadLiftT Lean.MetaM m] [inst : MonadControlT Lean.MetaM m] (input : Lean.Expr) (fn : Lean.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.

Equations

• Lean.Meta.forEachExpr' input fn = let x := { }; let x_1 := { monadLift := fun {α} x => liftM (liftM x) }; Lean.MonadCacheT.run (Lean.Meta.forEachExpr'.visit fn x x_1 input)

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

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

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

Equations

• Lean.Meta.forEachExpr e f = Lean.Meta.forEachExpr' e fun e => do f e pure true

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.

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.

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.