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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.traverseLambdaWithPos.visit f fvars p x = do let body ← f p (Lean.Expr.instantiateRev x fvars) liftM (Lean.Meta.mkLambdaFVars fvars body false true Lean.BinderInfo.implicit)

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.traverseForallWithPos.visit f fvars p x = do let body ← f p (Lean.Expr.instantiateRev x fvars) liftM (Lean.Meta.mkForallFVars fvars body false true Lean.BinderInfo.implicit)

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.traverseLetWithPos.visit f fvars p x = do let body ← f p (Lean.Expr.instantiateRev x fvars) liftM (Lean.Meta.mkLetFVars fvars body false Lean.BinderInfo.implicit)

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.

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

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

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

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

See also Lean.Core.traverseChildren.

Equations

• Lean.Meta.traverseChildren visit = Lean.Meta.forgetPos Lean.Meta.traverseChildrenWithPos visit