source
def Lean.Meta.traverseLambdaWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (f : SubExpr.Pos → Expr → M Expr) (p : SubExpr.Pos) (e : Expr) :
M Expr

Similar to `traverseLambda` but with an additional pos argument to track position.

Equations

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

Instances For

source
def Lean.Meta.traverseForallWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (f : SubExpr.Pos → Expr → M Expr) (p : SubExpr.Pos) (e : Expr) :
M Expr

Similar to `traverseForall` but with an additional pos argument to track position.

Equations

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

Instances For

source
def Lean.Meta.traverseLetWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (f : SubExpr.Pos → Expr → M Expr) (p : SubExpr.Pos) (e : Expr) :
M Expr

Similar to `traverseLet` but with an additional pos argument to track position.

Equations

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

Instances For

source
def Lean.Meta.traverseChildrenWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : SubExpr.Pos → Expr → M Expr) (p : SubExpr.Pos) (e : Expr) :
M Expr

Similar to `Lean.Meta.traverseChildren` except that `visit` also includes a `Pos` argument so you can track the subexpression position.

Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.traverseChildrenWithPos visit p (Lean.Expr.lam binderName binderType body binderInfo) = Lean.Meta.traverseLambdaWithPos visit p (Lean.Expr.lam binderName binderType body binderInfo)
- Lean.Meta.traverseChildrenWithPos visit p (Lean.Expr.letE declName type value body nondep) = Lean.Meta.traverseLetWithPos visit p (Lean.Expr.letE declName type value body nondep)
- Lean.Meta.traverseChildrenWithPos visit p (fn.app arg) = Lean.Expr.traverseAppWithPos visit p (fn.app arg)
- Lean.Meta.traverseChildrenWithPos visit p (Lean.Expr.mdata data b) = (Lean.Expr.mdata data b).updateMData! <$> visit p b
- Lean.Meta.traverseChildrenWithPos visit p (Lean.Expr.proj typeName idx b) = (Lean.Expr.proj typeName idx b).updateProj! <$> visit p.pushProj b
- Lean.Meta.traverseChildrenWithPos visit p e = pure e

Instances For

source
def Lean.Meta.traverseLambda {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : Expr → M Expr) (e : Expr) :
M Expr

Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run `f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, replacing each expression with the output of `f` and creating a new lambda. (that is, correctly instantiating bound variables and repackaging them after)

Equations

- Lean.Meta.traverseLambda visit = Lean.Meta.forgetPos✝ Lean.Meta.traverseLambdaWithPos visit

Instances For

source
def Lean.Meta.traverseForall {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : Expr → M Expr) (e : Expr) :
M Expr

Given an expression `(x₁ : α₁) → ... → (xₙ : αₙ) → b`, will run `f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, replacing the expression with the output of `f` and creating a new forall expression. (that is, correctly instantiating bound variables and repackaging them after)

Equations

- Lean.Meta.traverseForall visit = Lean.Meta.forgetPos✝ Lean.Meta.traverseForallWithPos visit

Instances For

source
def Lean.Meta.traverseLet {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : Expr → M Expr) (e : Expr) :
M Expr

Similar to `traverseLambda` and `traverseForall` but with let binders.

Equations

- Lean.Meta.traverseLet visit = Lean.Meta.forgetPos✝ Lean.Meta.traverseLetWithPos visit

Instances For

source
def Lean.Meta.traverseChildren {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : Expr → M Expr) (e : Expr) :
M Expr

Maps `visit` on each child of the given expression.

Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). So `traverseChildren f e` where `e = `(fn a₁ ... aₙ)` will return `(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))` rather than `(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`

See also `Lean.Core.traverseChildren`.

Equations

- Lean.Meta.traverseChildren visit = Lean.Meta.forgetPos✝ Lean.Meta.traverseChildrenWithPos visit

Instances For