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
andapply
replacerefine'
. 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
andapply
are more readable and (heuristically) tend to be more efficient on average.obtain
,rcases
andcases
replacecases'
. 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.
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.
refine'
, superseded byrefine
andapply
(controlled bylinter.style.refine
)cases'
, superseded byobtain
,rcases
andcases
(controlled bylinter.style.cases
)admit
, superseded bysorry
(controlled bylinter.style.admit
)
Equations
- One or more equations did not get rendered due to their size.