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.

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.

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.

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

The option linter.style.nativeDecide of the deprecated syntax linter flags usages of the native_decide tactic, which is disallowed in mathlib.

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

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.

def Mathlib.Linter.Style.getSetOptionMaxHeartbeatsComment : Lean.Syntax → Option (Lean.Name × Nat × Substring)

If the input syntax is of the form set_option <option> num in <string> cmd, where <option> contains maxHeartbeats, then it returns

• the <option>, as a name (typically, maxHeartbeats or synthInstance.maxHeartbeats);
• the number num and
• whatever is in <string>. Note that <string> can only consist of whitespace and comments.

Otherwise, it returns none.

Equations

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

def Mathlib.Linter.Style.isDecideNative (stx : Lean.Syntax) : Bool

Whether a given piece of syntax represents a decide tactic call with the native option enabled. This may have false negatives for decide (config := {<options>}) syntax).

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Linter.Style.isDecideNative stx = false

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)
• set_option maxHeartbeats, should contain an explanatory comment (controlled by linter.style.maxHeartbeats)

Equations

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