Commit 2025-11-21 22:06 82d756ea
View on Github →feat: privateModule linter (#31820)
This linter lints against nonempty modules that have only private declarations, and suggests adding @[expose] public section to the top.
This linter found 1 violation in Mathlib, which was fixed in #31822.