Documentation
Lean
.
Util
.
ReplaceLevel
Search
return to top
source
Imports
Lean.Expr
Imported by
Lean
.
Level
.
replace
Lean
.
Expr
.
ReplaceLevelImpl
.
cacheSize
Lean
.
Expr
.
ReplaceLevelImpl
.
State
Lean
.
Expr
.
ReplaceLevelImpl
.
ReplaceM
Lean
.
Expr
.
ReplaceLevelImpl
.
cache
Lean
.
Expr
.
ReplaceLevelImpl
.
replaceUnsafeM
Lean
.
Expr
.
ReplaceLevelImpl
.
replaceUnsafeM
.
visit
Lean
.
Expr
.
ReplaceLevelImpl
.
initCache
Lean
.
Expr
.
ReplaceLevelImpl
.
replaceUnsafe
Lean
.
Expr
.
replaceLevel
source
partial def
Lean
.
Level
.
replace
(
f?
:
Level
→
Option
Level
)
(
u
:
Level
)
:
Level
source
@[reducible, inline]
abbrev
Lean
.
Expr
.
ReplaceLevelImpl
.
cacheSize
:
USize
Equations
Instances For
source
structure
Lean
.
Expr
.
ReplaceLevelImpl
.
State
:
Type
keys :
Array
Expr
results :
Array
Expr
Instances For
source
@[reducible, inline]
abbrev
Lean
.
Expr
.
ReplaceLevelImpl
.
ReplaceM
(
α
:
Type
)
:
Type
Equations
Instances For
source
unsafe def
Lean
.
Expr
.
ReplaceLevelImpl
.
cache
(
i
:
USize
)
(
key
result
:
Expr
)
:
ReplaceM
Expr
Equations
Instances For
source
unsafe def
Lean
.
Expr
.
ReplaceLevelImpl
.
replaceUnsafeM
(
f?
:
Level
→
Option
Level
)
(
size
:
USize
)
(
e
:
Expr
)
:
ReplaceM
Expr
Equations
Instances For
source
unsafe def
Lean
.
Expr
.
ReplaceLevelImpl
.
replaceUnsafeM
.
visit
(
f?
:
Level
→
Option
Level
)
(
size
:
USize
)
(
e
:
Expr
)
:
ReplaceM
Expr
Equations
Instances For
source
unsafe def
Lean
.
Expr
.
ReplaceLevelImpl
.
initCache
:
State
Equations
Instances For
source
unsafe def
Lean
.
Expr
.
ReplaceLevelImpl
.
replaceUnsafe
(
f?
:
Level
→
Option
Level
)
(
e
:
Expr
)
:
Expr
Equations
Instances For
source
@[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]
partial def
Lean
.
Expr
.
replaceLevel
(
f?
:
Level
→
Option
Level
)
:
Expr
→
Expr