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.

def Lean.Expr.replaceRec (f? : (Lean.Expr → Lean.Expr) → Lean.Expr → Option Lean.Expr) : Lean.Expr → Lean.Expr

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