@[extern lean_replace_expr]

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

@[inline]

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

Equations

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

@[specialize #[]]

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