lean4-htt/tests
jrr6 836d7b703a
feat: add labeled subcomponents and helper functions for error messages (#8225)
This PR adds additional infrastructure for error message formatting.
Specifically, it adds convenience formatters for hints and notes,
including the ability to attach code actions to hint messages using a
"Try This"-like widget, along with several convenience formatters for
message data.

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
2025-05-07 21:15:27 +00:00
..
bench chore: robustify Nix shell (#8141) 2025-04-28 15:08:32 +00:00
compiler
elabissues
ir
lean feat: add labeled subcomponents and helper functions for error messages (#8225) 2025-05-07 21:15:27 +00:00
pkg feat: lean --setup (#8024) 2025-05-03 23:57:37 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain