# 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 : Lean.Expr → Lean.Expr) (e : Lean.Expr) => match f? r e with | some x => x | none => Lean.Expr.traverseChildren r e