Mathlib Changelog
v4
Changelog
About
Github
Structure
Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern
Modification history
2026-02-19 16:06
Mathlib/Tactic/Linter/UnusedInstancesInType.lean
feat: make the `unusedInstancesInType` linters fire when instances are not used outside of proofs in the type (#32440) …
Added
Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern
View on Github →