jrr6 4759506bcf chore: use note and hint' for message addenda (#8980) ... This PR improves the consistency of error message formatting by rendering addenda of several existing error messages as labeled notes and hints.		2025-06-27 15:16:01 +00:00
..
Prv
lakefile.lean
lean-toolchain
Prv.lean	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
test.sh