Commit 2026-10-06 14:58 4beb5491

perf(Linter): bundle instance linters into one linter (#44436) This PR bundles the three instance linters we have into a single linter for performance. The new linter lives in Mathlib.Tactic.Linter.DeclType, because it can accommodate any linter that acts on declaration types. Note: we could implement some kind of extensible framework for declaration type linters. But that could make the performance worse again. It would probably be more trouble than it's worth. This is in preparation for adding another instance linter: the concrete instance linter. After this PR, it should be possible to implement this with minimal performance cost.