logLint0Disable

Mathlib.Tactic.DeclarationNames

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

Lean4

/-- Used for linters which use `0` instead of `false` for disabling. -/
def logLint0Disable {m} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (linterOption : Lean.Option Nat)
    (stx : Syntax) (msg : MessageData) : m Unit :=
  let disable := .note m! "This linter can be disabled with `set_option {linterOption.name} 0`"
  logWarningAt stx (.tagged linterOption.name m! "{msg }{disable}")

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

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

Разделы

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

Аффилиация

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