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 replaces refine'. While they are similar, they handle metavariables slightly differently; this means that they are not completely interchangeable, nor can one completely replace the other. However, refine is more readable and (heuristically) tends 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.

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 and refine' are similar, but they handle meta-variables slightly differently. This means that they are not completely interchangeable, nor can one completely replace the other. However, refine is more readable and (heuristically) tends 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.

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.

Currently refine' (superseded by refine) and cases' (superseded by obtain, rcases and cases) are flagged. The linter can be turned off for these cases individually with the options linter.style.refine and linter.style.cases.

Equations

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