Documentation

Lean.Util.ReplaceExpr

source
@[extern lean_replace_expr]
opaque Lean.Expr.replaceImpl (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) :
Lean.Expr
source
@[inline]
def Lean.Expr.replace (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) :
Lean.Expr
Instances For
    source
    @[specialize #[]]
    def Lean.Expr.replaceNoCache (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) :
    Lean.Expr
    Instances For