Documentation
Lean
.
Linter
.
Deprecated
Search
Google site search
Lean
.
Linter
.
Deprecated
source
Imports
Init
Lean.Attributes
Lean.Linter.Basic
Lean.Elab.InfoTree.Main
Imported by
Lean
.
Linter
.
linter
.
deprecated
Lean
.
Linter
.
deprecatedAttr
Lean
.
Linter
.
isDeprecated
Lean
.
MessageData
.
isDeprecationWarning
Lean
.
Linter
.
getDeprecatedNewName
Lean
.
Linter
.
checkDeprecated
source
opaque
Lean
.
Linter
.
linter
.
deprecated
:
Lean.Option
Bool
source
opaque
Lean
.
Linter
.
deprecatedAttr
:
Lean.ParametricAttribute
(
Option
Lake.Name
)
source
def
Lean
.
Linter
.
isDeprecated
(env :
Lean.Environment
)
(declName :
Lake.Name
)
:
Bool
Instances For
source
def
Lean
.
MessageData
.
isDeprecationWarning
(msg :
Lean.MessageData
)
:
Bool
Instances For
source
def
Lean
.
Linter
.
getDeprecatedNewName
(env :
Lean.Environment
)
(declName :
Lake.Name
)
:
Option
Lake.Name
Instances For
source
def
Lean
.
Linter
.
checkDeprecated
{m :
Type
→
Type
}
[
Monad
m
]
[
Lean.MonadEnv
m
]
[
Lean.MonadLog
m
]
[
Lean.AddMessageContext
m
]
[
Lean.MonadOptions
m
]
(declName :
Lake.Name
)
:
m
Unit
Instances For