Syntax based linters

This file defines a linter that combines many different linters that each operate directly on the Syntax. This approach of combining the linters into a single loop is more efficient than having each linter do this by itself.

The cdot linter

opaque Mathlib.Linter.linter.style.cdot : Lean.Option Bool

The cdot linter flags uses of a dot (.) that could instead be a "cdot" (·). It also flags "isolated cdots", i.e. when the · is on its own line.

The dollarSyntax linter

opaque Mathlib.Linter.linter.style.dollarSyntax : Lean.Option Bool

The dollarSyntax linter flags uses of $ that could instead be <|. These are disallowed by the mathlib style guide, as using <| pairs better with |>.

The lambdaSyntax linter

opaque Mathlib.Linter.linter.style.lambdaSyntax : Lean.Option Bool

The lambdaSyntax linter flags uses of the symbol λ to define anonymous functions. This is syntactically equivalent to the fun keyword; mathlib style prefers using the latter.

The auxiliary declaration linter

opaque Mathlib.Linter.linter.auxLemma : Lean.Option Bool

The auxLemma linter flags explicit references to auto-generated "auxiliary" declarations such as _proof_1, match_1, or _sizeOf_1.

These names are internal implementation details generated by the Lean elaborator. They are not stable across refactors (e.g. reordering fields in a structure can renumber _proof_ indices), so depending on them makes code fragile.

The oldObtain linter, against stream-of-consciousness obtain

The oldObtain linter flags any occurrences of "stream-of-consciousness" obtain, i.e. uses of the obtain tactic which do not immediately provide a proof.

Example

There are six different kinds of obtain uses. In one example, they look like this.

theorem foo : True := by
  -- These cases are fine.
  obtain := trivial
  obtain h := trivial
  obtain : True := trivial
  obtain h : True := trivial
  -- These are linted against.
  obtain : True
  · trivial
  obtain h : True
  · trivial

We allow the first four (since an explicit proof is provided), but lint against the last two.

Why is this bad?

This is similar to removing all uses of Tactic.Replace and Tactic.Have from mathlib: in summary,

• this version is a Lean3-ism, which can be unlearned now
• the syntax obtain foo : type := proof is slightly shorter; particularly so when the first tactic of the proof is exact
• when using the old syntax as obtain foo : type; · proof, there is an intermediate state with multiple goals right before the focusing dot. This can be confusing.
• the old syntax could be slightly nicer when deferring goals: however, this is rare. In the 30 replacements of the last PR, this occurred twice. In both cases, the suffices tactic could also be used, as was in fact clearer.

opaque Mathlib.Linter.linter.oldObtain : Lean.Option Bool

The oldObtain linter flags uses of the "stream-of-consciousness" variants of the obtain tactic, i.e. with the proof postponed.

The extended binder linter

In mathlib we prefer writing the basic ∀/∃ binders over ∀ᵉ/∃ᵉ. This is because the latter was used quite infrequently, so the cost of needing to learn this notation was greater than the benefit.

opaque Mathlib.Linter.linter.style.extendedBinder : Lean.Option Bool

The extendedBinder linter flags uses of the ∀ᵉ/∃ᵉ notation for combining universal and existential binders. Mathlib prefers basic ∀/∃ notation.

The combined syntax linter