Def double__underscore

Modification history

2025-02-10 10:42
MathlibTest/DoubleUnderscore.lean
feat: lint declarations which contain a double underscore (#17580)
Added double__underscoreView on Github →