Documentation
Lean
.
Util
.
ReplaceExpr
Search
return to top
source
Imports
Lean.Expr
Lean.Util.PtrSet
Imported by
Lean.Elab.MutualInductive
Lean.Util
Lean.Meta.Tactic.FVarSubst
Lean.Compiler.CSimpAttr
Lean.Meta.Basic
Lean.Util.InstantiateLevelParams
Lean
.
Expr
.
replaceImpl
Lean
.
Expr
.
replace
Lean
.
Expr
.
replaceNoCache
source
@[extern lean_replace_expr]
opaque
Lean
.
Expr
.
replaceImpl
(
f?
:
Expr
→
Option
Expr
)
(
e
:
Expr
)
:
Expr
source
@[inline]
def
Lean
.
Expr
.
replace
(
f?
:
Expr
→
Option
Expr
)
(
e
:
Expr
)
:
Expr
Equations
Lean.Expr.replace
f?
e
=
Lean.Expr.replaceImpl
f?
e
source
@[specialize #[]]
def
Lean
.
Expr
.
replaceNoCache
(
f?
:
Expr
→
Option
Expr
)
(
e
:
Expr
)
:
Expr