Lean4
/-- 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. -/
def replaceRec (f? : (Expr → Expr) → Expr → Option Expr) : Expr → Expr :=
memoFix fun r e ↦
match f? r e with
| some x => x
| none => Id.run <| traverseChildren (pure <| r ·) e
