def Lean.Meta.traverseLambdaWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT Lean.MetaM M] [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} [Monad M] [MonadLiftT Lean.MetaM M] [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 (x.instantiateRev fvars) liftM (Lean.Meta.mkLambdaFVars fvars body)

def Lean.Meta.traverseForallWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT Lean.MetaM M] [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} [Monad M] [MonadLiftT Lean.MetaM M] [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 (x.instantiateRev fvars) liftM (Lean.Meta.mkForallFVars fvars body)

def Lean.Meta.traverseLetWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT Lean.MetaM M] [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} [Monad M] [MonadLiftT Lean.MetaM M] [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 (x.instantiateRev fvars) liftM (Lean.Meta.mkLetFVars fvars body false)

def Lean.Meta.traverseChildrenWithPos {M : Type → Type u_1} [Monad M] [MonadLiftT Lean.MetaM M] [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.
• 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

def Lean.Meta.traverseLambda {M : Type → Type u_1} [Monad M] [MonadLiftT Lean.MetaM M] [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} [Monad M] [MonadLiftT Lean.MetaM M] [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} [Monad M] [MonadLiftT Lean.MetaM M] [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} [Monad M] [MonadLiftT Lean.MetaM M] [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