fix: uses `PUnit`, `pure ()` forces implicit universe parameter to be `1` Remark: we should probably elaborate `def`s like we elaborate theorems when the resulting type is provided.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).