Lean4
/-- The deprecated syntax linter flags usages of deprecated syntax and suggests
replacement syntax. For each individual case, linting can be turned on or off separately.
* `refine'`, superseded by `refine` and `apply` (controlled by `linter.style.refine`)
* `cases'`, superseded by `obtain`, `rcases` and `cases` (controlled by `linter.style.cases`)
* `induction'`, superseded by `induction` (controlled by `linter.style.induction`)
* `admit`, superseded by `sorry` (controlled by `linter.style.admit`)
* `set_option maxHeartbeats`, should contain an explanatory comment
(controlled by `linter.style.maxHeartbeats`)
-/
def deprecatedSyntaxLinter : Linter where
run
stx := do
unless
getLinterValue linter.style.refine (← getLinterOptions) ||
getLinterValue linter.style.cases (← getLinterOptions) ||
getLinterValue linter.style.induction (← getLinterOptions) ||
getLinterValue linter.style.admit (← getLinterOptions) ||
getLinterValue linter.style.maxHeartbeats (← getLinterOptions) ||
getLinterValue linter.style.nativeDecide (← getLinterOptions) do
return
if (← MonadState.get).messages.hasErrors then
return
let deprecations := getDeprecatedSyntax stx
(withSetOptionIn fun _ ↦ do
for (kind, stx', msg) in deprecations do
match kind with
| ``Lean.Parser.Tactic.refine' =>
Linter.logLintIf linter.style.refine stx' msg
| `Mathlib.Tactic.cases' =>
Linter.logLintIf linter.style.cases stx' msg
| `Mathlib.Tactic.induction' =>
Linter.logLintIf linter.style.induction stx' msg
| ``Lean.Parser.Tactic.tacticAdmit =>
Linter.logLintIf linter.style.admit stx' msg
| ``Lean.Parser.Tactic.nativeDecide | ``Lean.Parser.Tactic.decide =>
Linter.logLintIf linter.style.nativeDecide stx' msg
| `MaxHeartbeats =>
Linter.logLintIf linter.style.maxHeartbeats stx' msg
| _ =>
continue)
stx
