Robert J. Simmons 31f09da88a feat: prioritize stuck synthetic MVar problems to improve error messages (#11184) ... This PR modifies the error message that is returned when more than one synthetic metavariable can't be resolved. The two heuristics used for prioritization are: - prefer typeclass problems associated with small ranges over typeclass problems associated with large ranges (I'm pretty confident in this heuristic) - do not prefer typeclass problems over other kinds of errors (not as confident in this heuristic)		2025-11-16 00:09:48 +00:00
..
bench	feat: verify all and any for hash maps (#10765)	2025-11-15 16:59:37 +00:00
compiler	fix: use general allocator for closures (#10982)	2025-10-27 10:16:59 +00:00
elabissues
ir
lake	fix: lake: indeterminism in targets test (#11188)	2025-11-15 04:20:24 +00:00
lean	feat: prioritize stuck synthetic MVar problems to improve error messages (#11184)	2025-11-16 00:09:48 +00:00
pkg	chore: make compilation type mismatch error message from non-exposed defs a lot less mysterious (#11177)	2025-11-14 10:50:43 +00:00
playground
plugin
simpperf
.gitignore
common.sh	chore: make workspaceSymbol benchmarks modules (#11094)	2025-11-05 18:40:39 +00:00
lakefile.toml
lean-toolchain