feat: `debug[cls] do` for debugging code This PR adds a simple framework for enabling debugging-only code (consistency checks or special options). Debug classes are similar to trace classes, but their options start with `debug` instead of `trace`. Adds `Meta.validateTypeCorrect` and `Meta.validateIsSort` as consistency check versions that avoid side effects and add context to any errors.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.