Declaration type linters

We bundle a number of linters that act on declaration types into a single linter:

• The overlapping instances linter
• The unused Fintype in type linter
• The unused Decidable in type linter

We bundle them because each of them acts on the Lean.Elab.Term.BodyInfo in the info tree, and it is expensive to do this search many times over.

These linters run even if the declaration contains an error. This is important because it means that a user will get a warning as soon as possible.

def Mathlib.Linter.declTypeLinter : Lean.Linter

Run all of the instance parameter linters. This linter collects the declaration bodies from the info trees, so that this work does not need to be duplicated.

Equations

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