Linter against deprecated syntax #
refine', cases' and induction' provide backward-compatible implementations of their
unprimed equivalents in Lean 3 –refine, cases and induction respectively.
They have been superseded by Lean 4 tactics:
refineandapplyreplacerefine'. While they are similar, they handle metavariables slightly differently; this means that they are not completely interchangeable, nor can one completely replace another. However,refineandapplyare more readable and (heuristically) tend to be more efficient on average.obtain,rcasesandcasesreplacecases'. Unlike the replacement tactics,cases'does not require the variables it introduces to be separated by case, which hinders readability.inductionreplacesinduction'for similar reasons tocasesandcases'.
The admit tactic is a synonym for the much more common sorry, so the latter should be preferred.
The native_decide tactic is not allowed in mathlib, as it trusts the entire Lean compiler
(and not just the Lean kernel). Because the latter is large and complicated, at present it is
probably possible to prove False using native_decide.
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.induction of the deprecated syntax linter flags usages of
the induction' tactic, which is a backward-compatible version of Lean 3's induction tactic.
Unlike Lean 4's induction, variables introduced by induction' 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.
The option linter.style.nativeDecide of the deprecated syntax linter flags usages of
the native_decide tactic, which is disallowed in mathlib.
The option linter.style.maxHeartbeats of the deprecated syntax linter flags usages of
set_option <name-containing-maxHeartbeats> n in cmd that do not add a comment explaining
the reason for the modification of the maxHeartbeats.
This includes set_option maxHeartbeats n in and set_option synthInstance.maxHeartbeats n in.