ErrorFormat

Mathlib.Tactic.Linter.TextBased

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

Lean4

/-- How to format style errors -/
inductive ErrorFormat/-- Produce style error output aimed at humans: no error code, clickable file name -/

  | humanReadable : ErrorFormat/--
Produce an entry in the style-exceptions file: mention the error code, slightly uglier
  than human-readable output -/

  | exceptionsFile : ErrorFormat/-- Produce output suitable for Github error annotations: in particular,
  duplicate the file path, line number and error code -/

  | github : ErrorFormat
  deriving BEq

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

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

Разделы

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

Аффилиация

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