upstreamableDecl

Mathlib.Tactic.Linter.UpstreamableDecl

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

Lean4

/-- The `upstreamableDecl` linter detects declarations that could be moved to a file higher up in the
import hierarchy. If this is the case, it emits a warning.

By default, this linter will not fire on definitions, nor private declarations:
see options `linter.upstreamableDecl.defs` and `linter.upstreamableDecl.private`.

This is intended to assist with splitting files.
-/
@[init initFn✝, ]
opaque upstreamableDecl : Lean.Option✝ Bool

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

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

Разделы

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

Аффилиация

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