lean4-htt/tests
jrr6 43aec5b254
fix: improve error-message hint rendering and API (#8486)
This PR improves the rendering of hints in error messages by
consistently indenting diffs and splitting large diffs less granularly;
it also improves the ergonomics of `Lean.MessageData.hint`. Note that
the changes to the signature of `Lean.MessageData.hint` are breaking.

This PR depends on #8457.
2025-06-01 01:22:09 +00:00
..
bench chore: try refining some benchmark settings (#8377) 2025-05-16 11:24:11 +00:00
compiler
elabissues
ir
lean fix: improve error-message hint rendering and API (#8486) 2025-06-01 01:22:09 +00:00
pkg feat: do not export def bodies by default (#8221) 2025-05-15 12:16:54 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain