Def Mathlib.Linter.privateModule

Modification history

2025-11-21 22:06
Mathlib/Tactic/Linter/PrivateModule.lean
feat: `privateModule` linter (#31820) …
Added Mathlib.Linter.privateModuleView on Github →