Def Mathlib.Linter.privateModule

Modification history

2026-10-05 16:14
Mathlib/Tactic/Linter/PrivateModule.lean
chore(Linter): use `ModuleLinter` for `missingEnd` and `privateModule` (#44517) …
Modified Mathlib.Linter.privateModuleView on Github →
2025-11-21 22:06
Mathlib/Tactic/Linter/PrivateModule.lean
feat: `privateModule` linter (#31820) …
Added Mathlib.Linter.privateModuleView on Github →