Documentation
Lean
.
Meta
.
Reduce
Search
Google site search
Lean
.
Meta
.
Reduce
source
Imports
Init
Lean.Meta.Basic
Lean.Meta.FunInfo
Lean.Util.MonadCache
Imported by
Lean
.
Meta
.
reduce
Lean
.
Meta
.
reduce
.
visit
Lean
.
Meta
.
reduceAll
source
def
Lean
.
Meta
.
reduce
(e :
Lean.Expr
)
(explicitOnly :
optParam
Bool
true
)
(skipTypes :
optParam
Bool
true
)
(skipProofs :
optParam
Bool
true
)
:
Lean.MetaM
Lean.Expr
Instances For
source
partial def
Lean
.
Meta
.
reduce
.
visit
(explicitOnly :
optParam
Bool
true
)
(skipTypes :
optParam
Bool
true
)
(skipProofs :
optParam
Bool
true
)
(e :
Lean.Expr
)
:
Lean.MonadCacheT
Lean.Expr
Lean.Expr
Lean.MetaM
Lean.Expr
source
def
Lean
.
Meta
.
reduceAll
(e :
Lean.Expr
)
:
Lean.MetaM
Lean.Expr
Instances For