errorMessage

Mathlib.Tactic.Linter.TextBased

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

Lean4

/-- Create the underlying error message for a given `StyleError`. -/
def errorMessage (err : StyleError) : String :=
  match err with
  | StyleError.adaptationNote =>
    "Found the string \"Adaptation note:\", please use the #adaptation_note command instead"
  | windowsLineEnding =>
    "This line ends with a windows line ending (\r\n): please use Unix line\
          endings (\n) instead"
  | trailingWhitespace => "This line ends with some whitespace: please remove this"
  | semicolon => "This line contains a space before a semicolon"

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

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

Разделы

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

Аффилиация

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