Theorem double__underscore

Modification history

2026-06-30 18:26
MathlibTest/Linter/DupNamespace.lean
chore(MathlibTest): move test files for linters into the Linter subdirectory (#40397) …
Deleted double__underscoreView on Github →
2025-02-10 10:42
MathlibTest/Lint.lean
feat: lint declarations which contain a double underscore (#17580)
Added double__underscoreView on Github →