Banning anonymous constructors for a certain type

Stream: lean4

[Eric Wieser]

Would it possible to make it a linter error to use anonymous constructor notation for certain types? In particular, I'm thinking of things like docs#RingHom where to correctly nest the angle brackets, you need to know precisely what the extends keyword is doing

[Yaël Dillies]

Sorry, I'm probably guilty of those :grinning_face_with_smiling_eyes:

[Eric Wieser]

#7015 has some examples of the type of code this linter would remove.