linter for non-reducible non-instance defs

Stream: mathlib4

[Jireh Loreaux]

We try to follow the library note which says that when you implement a non-instance of a class as a def (doesn't apply to Prop-valued classes), so that it can be later used to create an actual instance, then it should be marked @[reducible] (a.k.a. abbrev).

Can I entice someone to write a linter for this? I'm asking because I just found out that docs#MetricSpace.replaceUniformity and friends are not reducible, which I'm about to go fix, but I had to find out the hard way that this was missing.

[Damiano Testa]

Jireh, I have currently lots of dangling projects. I would be happy to write such a linter, but I need some time to catch up on my loose ends!

[Damiano Testa]

If no one is working on this in a couple of weeks, feel free to remind me! :smile:

[Matthew Ballard]

I think this is just completely broken across the library at the moment. Sometimes for good reasons (eg something is actually irreducible for performance reasons) and often dependent on the conventions of the area.