StyleError

Mathlib.Tactic.Linter.TextBased

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

Lean4

/-- Possible errors that text-based linters can report. -/
-- We collect these in one inductive type to centralise error reporting.

inductive StyleError where/-- The bare string "Adaptation note" (or variants thereof):
  instead, the #adaptation_note command should be used. -/

  | adaptationNote/-- A line ends with windows line endings (\r\n) instead of unix ones (\n). -/

  | windowsLineEnding/-- A line contains trailing whitespace. -/

  | trailingWhitespace/-- A line contains a space before a semicolon -/

  | semicolon
  deriving BEq

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

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

Разделы

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

Аффилиация

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