module

Mathlib.Tactic.Linter.DeprecatedModule

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.linter.deprecated.module

Lean4

/-- The `deprecated.module` linter emits a warning when a file that has been renamed or split
is imported.
The default value is `true`, since this linter is designed to warn projects downstream of `Mathlib`
of refactors and deprecations in `Mathlib` itself.
-/
@[init initFn✝, ]
opaque module : Lean.Option✝ Bool

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

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

Разделы

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

Аффилиация

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