Def Mathlib.Linter.UnusedInstancesInType.unusedFintypeInType

Modification history

2026-10-06 14:58
Mathlib/Tactic/Linter/UnusedInstancesInType.lean
perf(Linter): bundle instance linters into one linter (#44436) …
Deleted Mathlib.Linter.UnusedInstancesInType.unusedFintypeInTypeView on Github →
2026-01-15 16:12
Mathlib/Tactic/Linter/UnusedInstancesInType.lean
feat: `unusedFintypeInType` linter (#31794) …
Added Mathlib.Linter.UnusedInstancesInType.unusedFintypeInTypeView on Github →