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. They are registered as linters in Mathlib.Tactic.Linter.DeclType.

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

@[deprecated Lean.withSetOptionIn (since := "2026-10-05")]

partial def Mathlib.Linter.UnusedInstancesInType.withSetBoolOptionIn (x : Lean.Elab.Command.CommandElab) : Lean.Elab.Command.CommandElab

withSetOptionIn used to break infotree searches, this is fixed in lean4#11313.

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.

def Mathlib.Linter.UnusedInstancesInType.unusedDecidableInType (thm : Lean.ConstantVal) (bodyRef : Lean.Syntax) : Lean.CoreM Unit

Detect Decidable* instance hypotheses in the type of thm which are not used in the remainder of the type, and suggest replacing them with a use of classical in the proof or open scoped Classical in at the term level.

Equations

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

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

The unusedFintypeInType linter checks if a theorem's hypotheses include Fintype instances which are not used in the remainder of the type. If so, it suggests modifying the instances to Finite _ and using Fintype.ofFinite in the proof, or removing them entirely.

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

def Mathlib.Linter.UnusedInstancesInType.unusedFintypeInType (thm : Lean.ConstantVal) (bodyRef : Lean.Syntax) : Lean.CoreM Unit

Detect Fintype instance hypotheses in the type of thm which are not used in the remainder of the type, and suggest replacing them with the corresponding hypothesis of Finite and the use of Fintype.ofFinite in the proof.

Equations

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