Lean.Meta.ExprTraverse

source

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

M Lean.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

source

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

Lean.Expr → M Lean.Expr

source

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

M Lean.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

source

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

Lean.Expr → M Lean.Expr

source

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

M Lean.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

source

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

Lean.Expr → M Lean.Expr

source

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

M Lean.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.

source

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

M Lean.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

source

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

M Lean.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

source

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

M Lean.Expr

Similar to traverseLambda and traverseForall but with let binders.

Equations

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

source

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

M Lean.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ₙ))