show_deprecated_modules

Mathlib.Tactic.Linter.DeprecatedModule

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.command#show_deprecated_modules

Lean4

/-- A utility command to show the current entries of the `deprecatedModuleExt` in the format:
```
Deprecated modules

'MathlibTest.DeprecatedModule' deprecates to
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
with message 'We can also give more details about the deprecation'

...
```
-/
@[command_parser 1000]
public meta def «command#show_deprecated_modules» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Linter.«command#show_deprecated_modules» 1024
    (ParserDescr.symbol✝ "#show_deprecated_modules")

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru