Lean.Meta.ExprTraverse

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

Instances For

source

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

Expr → M Expr

Equations

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

Instances For

source

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

Expr → M Expr

Equations

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

Instances For

source

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

Expr → M Expr

Equations

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

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

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

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

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ₙ))