Expression Lenses

Functions for manipulating subexpressions using SubExpr.Pos.

def Lean.Meta.replaceSubexpr {M : Type → Type} [Monad M] [MonadLiftT Lean.MetaM M] [MonadControlT Lean.MetaM M] [Lean.MonadError M] (replace : Lean.Expr → M Lean.Expr) (p : Lean.SubExpr.Pos) (root : Lean.Expr) : M Lean.Expr

Run the given replace function to replace the expression at the subexpression position. If the subexpression is below a binder the bound variables will be appropriately instantiated with free variables and reabstracted after the replacement. If the subexpression is invalid or points to a type then this will throw.

Equations

• Lean.Meta.replaceSubexpr replace p root = Lean.Meta.lensAux replace p.toArray.toList root

def Lean.Meta.viewSubexpr {M : Type → Type} [Monad M] [MonadLiftT Lean.MetaM M] [MonadControlT Lean.MetaM M] [Lean.MonadError M] {α : Type} (visit : Array Lean.Expr → Lean.Expr → M α) (p : Lean.SubExpr.Pos) (root : Lean.Expr) : M α

view visit p e runs visit fvars s where s : Expr is the subexpression of e at p. and fvars are the free variables for the binders that s is under. s is already instantiated with respect to these. The role of the visit function is analogous to the k function in Lean.Meta.forallTelescope.

Equations

• Lean.Meta.viewSubexpr visit p root = Lean.Meta.viewAux visit #[] p.toArray.toList root

def Lean.Meta.foldAncestors {M : Type → Type} [Monad M] [MonadLiftT Lean.MetaM M] [MonadControlT Lean.MetaM M] [Lean.MonadError M] {α : Type} (k : Array Lean.Expr → Lean.Expr → Nat → α → M α) (init : α) (p : Lean.SubExpr.Pos) (e : Lean.Expr) : M α

foldAncestors k init p e folds over the strict ancestor subexpressions of the given expression e above position p, starting at the root expression and working down. The fold function k is given the newly instantiated free variables, the ancestor subexpression, and the coordinate that will be explored next.

Equations

• Lean.Meta.foldAncestors k init p e = Lean.Meta.foldAncestorsAux k init p.toArray.toList #[] e

def Lean.Core.viewSubexpr {M : Type → Type} [Monad M] [Lean.MonadError M] (p : Lean.SubExpr.Pos) (root : Lean.Expr) : M Lean.Expr

Given a valid SubExpr, return the raw current expression without performing any instantiation. If the given SubExpr has a type subexpression coordinate, then throw an error.

This is a cheaper version of Lean.Meta.viewSubexpr and can be used to quickly view the subexpression at a position. Note that because the resulting expression may contain loose bound variables it can't be used in any MetaM methods.

Equations

• Lean.Core.viewSubexpr p root = Lean.SubExpr.Pos.foldlM Lean.Core.viewCoordRaw root p

def Lean.Core.viewBinders {M : Type → Type} [Monad M] [Lean.MonadError M] (p : Lean.SubExpr.Pos) (root : Lean.Expr) : M (Array (Lake.Name × Lean.Expr))

viewBinders p e returns a list of all of the binders (name, type) above the given position p in the root expression e

Equations

• One or more equations did not get rendered due to their size.

def Lean.Core.numBinders {M : Type → Type} [Monad M] [Lean.MonadError M] (p : Lean.SubExpr.Pos) (e : Lean.Expr) : M Nat

Returns the number of binders above a given subexpr position.

Equations

• Lean.Core.numBinders p e = Array.size <$> Lean.Core.viewBinders p e