feat: display diagnostic information at term and tactic `set_option diagnostics true`

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

leodemoura commented 2 weeks ago

We don't need to include reduction info at simp diagnostic information.

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 e1b798483608d61a5abd5f39cb60969bb35df0cb --onto 83c139f7504706624eb3dcb3d78000d4fc6f4d13. (2024-05-01 22:49:58)