Linters for Unused Instances in Types

This file declares linters which detect certain instance hypotheses in declarations that are unused in the remainder of the type.

Currently, these linters only handle theorems. (This also includes lemmas and instances of Prop classes.)

• unusedDecidableInType linter (currently off by default): suggests replacing type-unused Decidable* instance hypotheses, and could therefore be replaced by classical in the proof.

TODO: log on type signature instead of whole command TODO: add more linters! TODO: create Try This suggestions

opaque Mathlib.Linter.UnusedInstancesInType.linter.unusedDecidableInType : Lean.Option Bool

The unusedDecidableInType linter checks if a theorem's hypotheses include Decidable* instances which are not used in the remainder of the type. If so, it suggests removing the instances and using classical or open scoped Classical in, as appropriate, in the theorem's proof instead.

This linter fires only on theorems. (This includes lemmas and instances of Prop classes.)

Note: set_option linter.unusedDecidableInType _ in <command> currently only works at the outermost level of a command due to working around lean4#11313.