Theorem fooUsing

Modification history

2026-02-19 16:06
MathlibTest/UnusedInstancesInType/Decidable.lean
feat: make the `unusedInstancesInType` linters fire when instances are not used outside of proofs in the type (#32440) …
Modified fooUsingView on Github →
2026-01-15 16:12
MathlibTest/UnusedInstancesInType/Fintype.lean
feat: `unusedFintypeInType` linter (#31794) …
Added fooUsingView on Github →
2025-11-25 19:25
MathlibTest/UnusedInstancesInType.lean
feat(Linter): port unused `Decidable*` instance hypothesis linter (#31142) …
Added fooUsingView on Github →