batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: apply dupNamespace linter to instances

Open Ruben-VandeVelde opened this issue 1 year ago • 4 comments

This caught 14 bugs with no false positives over in https://github.com/leanprover-community/mathlib4/pull/10899

Ruben-VandeVelde avatar Feb 23 '24 21:02 Ruben-VandeVelde

How does this interact with deriving instance ... and other automatically generated instances?

fgdorais avatar Feb 25 '24 04:02 fgdorais

I don't know, but I have no reason to suspect those would introduce duplicate namespaces. If there's a way to exclude those, that's fine by me, of course.

Ruben-VandeVelde avatar Feb 25 '24 20:02 Ruben-VandeVelde

How about adding some tests?

fgdorais avatar Feb 25 '24 22:02 fgdorais

The test doesn't seem to include a result from the linter? Can you use #guard_msgs?

kim-em avatar Apr 24 '24 03:04 kim-em