oldObtainLinter

Mathlib.Tactic.Linter.OldObtain

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

Lean4

/-- The `oldObtain` linter: see docstring above -/
def oldObtainLinter : Linter where
  run :=
    withSetOptionIn fun stx => do
      unless getLinterValue linter.oldObtain (← getLinterOptions) do
        return
      if (← MonadState.get).messages.hasErrors then
        return
      if let some head := stx.find? isObtainWithoutProof then
        Linter.logLint linter.oldObtain head m!"Please remove stream-of-consciousness `obtain` syntax"

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

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

Разделы

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

Аффилиация

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