firstNonImport?

Mathlib.Tactic.Linter.Header

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.firstNonImport?

Lean4

/-- `firstNonImport? stx` assumes that the input `Syntax` is of kind `Lean.Parser.Module.module`.
It returns
* `none`, if `stx` consists only of `import` statements,
* the first non-`import` command in `stx`, otherwise.

The intended use-case is to use the output of `testParseModule` as the input of
`firstNonImport?`.
-/
def firstNonImport? : Syntax → Option Syntax
  | .node _ ``Lean.Parser.Module.module #[_header, .node _ `null args] => args[0]?
  | _ => some .missing

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

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

Разделы

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

Аффилиация

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