Documentation

Mathlib.Tactic.Linter.DeprecatedSyntaxLinter

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:

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.

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.

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.

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.

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

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.

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