mathlibStandardSet

Mathlib.Init

URI: https://scilib.ai/kg/mathlib#linter.mathlibStandardSet

Lean4

/-- Define a linter set of all mathlib syntax linters which are enabled by default.

Projects depending on mathlib can use `set_option linter.allMathlibLinters true` to enable
all these linters, or add the `weak.linter.mathlibStandardSet` option to their lakefile.
-/
@[init initFn✝, ]
opaque mathlibStandardSet : Lean.Option✝ Bool✝

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

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

Разделы

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

Аффилиация

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