Expression Lenses #
Functions for manipulating subexpressions using
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.
view visit p e runs
visit fvars s where
s : Expr is the subexpression of
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
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.
Given a valid SubExpr, will return the raw current expression without performing any instantiation. If the SubExpr has a type subexpression coordinate then will 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 will contain
loose bound variables it can't be used in any