Kim Morrison 4b28713a44 feat: #grind_lint check produces a "Try this:" suggestion with #grind_list inspect commands (#11204) ... This PR has `#grind_list check` produce a "Try this:" suggestion with `#grind_list inspect` commands, as this is usually the next step in dealing with problematic cases. We also fix the grind pattern for one theorem, as part of testing the workflow. More to follow.		2025-11-17 00:52:57 +00:00
..
bench	test: benchmark for large partial match (#11199)	2025-11-16 11:20:31 +00:00
compiler
elabissues
ir
lake	fix: lake: indeterminism in targets test (#11188)	2025-11-15 04:20:24 +00:00
lean	feat: #grind_lint check produces a "Try this:" suggestion with #grind_list inspect commands (#11204)	2025-11-17 00:52:57 +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