@[extern lean_replace_expr]

opaque Lean.Expr.replaceImpl (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr

@[inline]

def Lean.Expr.replace (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr

Equations

• Lean.Expr.replace f? e = Lean.Expr.replaceImpl f? e

@[specialize #[]]

def Lean.Expr.replaceNoCache (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr