fix: keep auxiliary names for private declarations private This PR limits public auxiliary naming to the module-level name generator and adds coverage for helper visibility under `import all`.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.