Def Uses

Modification history

2026-02-19 16:06

MathlibTest/UnusedInstancesInType/Basic.lean

feat: make the `unusedInstancesInType` linters fire when instances are not used outside of proofs in the type (#32440) …

Deleted Uses View on Github →

2026-01-15 16:12

MathlibTest/UnusedInstancesInType/Basic.lean

feat: `unusedFintypeInType` linter (#31794) …

Modified Uses View on Github →

2025-11-25 19:25

MathlibTest/UnusedInstancesInType.lean

feat(Linter): port unused `Decidable*` instance hypothesis linter (#31142) …

Added Uses View on Github →