source
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`.

Equations

- Lean.Meta.visitLambda f e = Lean.Meta.visitLambda.visit✝ f #[] e

Instances For

source
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`.

Equations

- Lean.Meta.visitForall f e = Lean.Meta.visitForall.visit✝ f #[] e

Instances For

source
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`.

Equations

- Lean.Meta.visitLet f e = Lean.Meta.visitLet.visit✝ f #[] e

Instances For

source
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.

Equations

- Lean.Meta.forEachExpr' input fn = (Lean.Meta.forEachExpr'.visit✝ fn { } { monadLift := fun {α : Type} (x : ST IO.RealWorld α) => liftM (liftM x) } input).run

Instances For

source
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.

Equations

- Lean.Meta.forEachExpr e f = Lean.Meta.forEachExpr' e fun (e : Lean.Expr) => do f e pure true

Instances For

source
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.

Equations

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

Instances For

source
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`

Equations

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

Instances For

source
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 type 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