Private module linter

This linter lints against nonempty modules that have only private declarations, and suggests adding @[expose] public section to the top or selectively marking declarations as public.

Implementation notes

env.constants.map₂ contains all locally-defined constants, and accessing this waits until all declarations are added. By linting (only) the eoi token, we can capture all constants defined in the file.

Note that private declarations are exactly those which satisfy isPrivateName, whether private due to an explicit private or due to not being made public.

opaque Mathlib.Linter.linter.privateModule : Lean.Option Bool

The privateModule linter lints against nonempty modules that have only private declarations, and suggests adding @[expose] public section or selectively marking declarations as public.