checkpoint This is broken. We need special treatment during name resolution and declaration elaboration. Parts of the code base are making the assumption that private names and macro scopes are different things.
This is the repository for Lean 4, which is currently being released as milestone releases towards a first stable release. Lean 3 is still the latest stable release.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.