header

Mathlib.Tactic.Linter.Header

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

Lean4

/-- The "header" style linter checks that a file starts with
```
/-
Copyright ...
Apache ...
Authors ...
-/

import statements*
module doc-string*
remaining file
```
It emits a warning if
* the copyright statement is malformed;
* `Mathlib.Tactic` is imported;
* any import in `Lake` is present;
* the first non-`import` command is not a module doc-string.

The linter allows `import`-only files and does not require a copyright statement in `Mathlib.Init`.
-/
@[init initFn✝, ]
opaque header : Lean.Option✝ Bool

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

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

Разделы

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

Аффилиация

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