deprecatedNoSince

Mathlib.Tactic.Linter.Lint

URI: https://scilib.ai/kg/mathlib#Batteries.Tactic.Lint.deprecatedNoSince

Lean4

/-- Linter that check that all `deprecated` tags come with `since` dates. -/
@[env_linter]
def deprecatedNoSince : Linter
    where
  noErrorsFound := "no `deprecated` tags without `since` dates."
  errorsFound := "FOUND `deprecated` tags without `since` dates."
  test
    declName := do
    let some info := Lean.Linter.deprecatedAttr.getParam? (← getEnv) declName |
      return none
    match info.since? with
    | some _ =>
      return none
    | none =>
      return m!"`deprecated` attribute without `since` date"

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

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

Разделы

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

Аффилиация

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