Linter against deprecated syntax

refine' and cases' provide backward-compatible implementations of their unprimed equivalents in Lean 3, refine and cases. They have been superseded by Lean 4 tactics:

• refine and apply replace refine'. While they are similar, they handle metavariables slightly differently; this means that they are not completely interchangeable, nor can one completely replace another. However, refine and apply are more readable and (heuristically) tend to be more efficient on average.
• obtain, rcases and cases replace cases'. Unlike the replacement tactics, cases' does not require the variables it introduces to be separated by case, which hinders readability.

The admit tactic is a synonym for the much more common sorry, so the latter should be preferred.

This linter is an incentive to discourage uses of such deprecated syntax, without being a ban. It is not inherently limited to tactics.

opaque Mathlib.Linter.Style.linter.style.refine : Lean.Option Bool

The option linter.style.refine of the deprecated syntax linter flags usages of the refine' tactic.

The tactics refine, apply and refine' are similar, but they handle metavariables slightly differently. This means that they are not completely interchangeable, nor can one completely replace another. However, refine and apply are more readable and (heuristically) tend to be more efficient on average.

opaque Mathlib.Linter.Style.linter.style.cases : Lean.Option Bool

The option linter.style.cases of the deprecated syntax linter flags usages of the cases' tactic, which is a backward-compatible version of Lean 3's cases tactic. Unlike obtain, rcases and Lean 4's cases, variables introduced by cases' are not required to be separated by case, which hinders readability.

opaque Mathlib.Linter.Style.linter.style.admit : Lean.Option Bool

The option linter.style.admit of the deprecated syntax linter flags usages of the admit tactic, which is a synonym for the much more common sorry.

partial def Mathlib.Linter.Style.getDeprecatedSyntax : Lean.Syntax → Array (Lean.SyntaxNodeKind × Lean.Syntax × Lean.MessageData)

getDeprecatedSyntax t returns all usages of deprecated syntax in the input syntax t.

def Mathlib.Linter.Style.deprecatedSyntaxLinter : Lean.Linter

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)
• admit, superseded by sorry (controlled by linter.style.admit)

Equations

• One or more equations did not get rendered due to their size.