Commit 2025-11-25 19:25 c36d1388

feat(Linter): port unused Decidable* instance hypothesis linter (#31142) This PR ports the decidableClassical linter from mathlib3 which detects Decidable* instances in the type of a theorem that are unused in the remainder of the type, and can therefore be replaced with classical in the proof. Prior art: #10235, by @urkud. This is an open pull request from over a year ago that has slowed down, but fulfills a similar purpose. There is a major difference: #10235 contributes an env_linter that does not run interactively, while the current PR is a syntax linter that runs while editing. In this PR, we lint only user-written theorems (including theorems, lemmas, and instances of Prop classes) by looking for elaborated declarations in the infotree. This opens us up to better logging and try-this suggestions. (While this PR is written with future expansion in mind, these tasks require developing the meta API a bit further and are left to subsequent PRs.) The infrastructure here is generic to unused instances in the remainder of a type, and can easily be used to write the other FinType, Encodable, etc. linters. We rename the linter from decidableClassical to unusedDecidableInType with the intention of naming all future related linters according to the same pattern. This PR does not turn the linter on; it is off by default. Turning the linter on is performed in #31747. Discussed in part on Zulip here. In recognition of the work on #10235, and its influence on this PR: