checkpoint Failed attempt to construct missing `Repr` instances recursively. The correct solution is to track the reason for a TC failure. Or, add support at the TC procedure for generating "missing instances". That is, when `TC` fails to find global instances for `Repr Foo`, it tries to invoke the `deriving` handler. It seems a bit crazy.
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.