ReplaceRec #
We define a more flexible version of Expr.replace
where we can use recursive calls even when
replacing a subexpression. We completely mimic the implementation of Expr.replace
.
A version of Expr.replace
where the replacement function is available to the function f?
.
replaceRec f? e
will call f? r e
where r = replaceRec f?
.
If f? r e = none
then r
will be called on each immediate subexpression of e
and reassembled.
If it is some x
, traversal terminates and x
is returned.
If you wish to recursively replace things in the implementation of f?
, you can apply r
.
The function is also memoised, which means that if the same expression (by reference) is encountered the cached replacement is used.
Equations
- Lean.Expr.replaceRec f? = memoFix fun r e => match f? r e with | some x => x | none => Lean.Expr.traverseChildren r e