feat: `set_option diagnostics true` for `simp`, and structured diagnostic messages

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

Closed leodemoura closed 2 weeks ago

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cc2ccf71d5247c240cdc93fa9aee9b144f6ed3ee --onto 1630d9b803164bb522f4a40fbc8fbf104cca425e. (2024-05-01 01:05:31)