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
def Lean.Expr.replaceRec (f? : (Lean.Expr → Lean.Expr) → Lean.Expr → Option Lean.Expr) :
A version of
Expr.replace where the replacement function is available to the function
replaceRec f? e will call
f? r e where
r = replaceRec f?.
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
The function is also memoised, which means that if the same expression (by reference) is encountered the cached replacement is used.
- Lean.Expr.replaceRec f? = memoFix fun r e => match f? r e with | some x => x | none => Lean.Expr.traverseChildren r e