TextbasedLinter

Mathlib.Tactic.Linter.TextBased

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.TextBased.TextbasedLinter

Lean4

/-- Core logic of a text based linter: given a collection of lines,
return an array of all style errors with line numbers. If possible,
also return the collection of all lines, changed as needed to fix the linter errors.
(Such automatic fixes are only possible for some kinds of `StyleError`s.)
-/
abbrev TextbasedLinter :=
  LinterOptions → Array String → Array (StyleError × ℕ) × (Option (Array String))

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

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

Разделы

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

Аффилиация

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