RFC: private sections

[mcdoll]

Private sections

Add support for private sections within public sections.

• User Experience: How does this feature improve the user experience?
  At the moment it is confusing that the private and the public keyword work in different contexts, in particular
  private section failing with a confusing error message.

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?
  In mathlib most code is public, so many files start with a @[expose] public section. If a file has a section that is just for a specific goal, but not needed further down the line, then one has to manually tag all definitions and theorems with private, see for example
  [Merged by Bors] - chore(Analysis/SchwartzSpace): make some definitions private leanprover-community/mathlib4#34552

Community Feedback

Discussion:
#mathlib4 > Mathlib has moved to the new module system @ 💬

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.