feat: add `Grind.Config.verbose` and `reportIssue!` macro This PR adds the `grind` configuration option `verbose`. For example, `grind -verbose` disables all diagnostics. We are going to use this flag to implement `try?`.
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).