Kyle Miller 7cd406f335 fix: check is valid structure projection when pretty printing (#4982) ... For structure projections, the pretty printer assumed that the expression was type correct. Now it checks that the object being projected is of the correct type. Such terms appear in type mismatch errors. Also, fixes and improves `#print` for structures. The types of projections now use MessageData (so are now hoverable), and the type of `self` is now the correct type. Closes #4670		2024-08-12 15:52:17 +00:00
..
bench	chore: reduce stack space usage at instantiate_mvars_fn (#4931)	2024-08-06 17:38:59 +00:00
compiler	fix: split libleanshared on Windows to avoid symbol limit	2024-08-12 14:14:42 +02:00
elabissues
ir
lean	fix: check is valid structure projection when pretty printing (#4982)	2024-08-12 15:52:17 +00:00
pkg	feat: accept user-defined options on the cmdline (#4741)	2024-08-02 12:24:56 +00:00
playground	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508)	2024-03-04 23:56:30 +00:00
plugin	chore: when a linter crashes, prefix its name (#4967)	2024-08-12 02:36:42 +00:00
simpperf
.gitignore
common.sh
lean-toolchain