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) …
Added fooUsing₁'View on Github →