Kim Morrison b7520e7232 chore: cleanup grind annotations in List (#10338) ... This PR updates `@[grind]` annotations which should be `@[grind =]`, for robustness (and, presumably, in some fraction of cases the existing heuristic for `@[grind]` is already too liberal).		2025-09-11 02:36:18 +00:00
..
Lex	refactor: improve names in the range API (#10059)	2025-09-05 13:10:05 +00:00
QSort	feat: integrate high-level order typeclasses with BEq and Ord (#9908)	2025-08-19 07:54:53 +00:00
Subarray	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Attach.lean	chore: cleanup grind annotations in List (#10338)	2025-09-11 02:36:18 +00:00
Basic.lean	chore: cleanup grind annotations in List (#10338)	2025-09-11 02:36:18 +00:00
BasicAux.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
BinSearch.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Bootstrap.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Count.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
DecidableEq.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Erase.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Extract.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Find.lean	chore: cleanup grind annotations in List (#10338)	2025-09-11 02:36:18 +00:00
FinRange.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
GetLit.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
InsertIdx.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
InsertionSort.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Lemmas.lean	chore: cleanup grind annotations in List (#10338)	2025-09-11 02:36:18 +00:00
Lex.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
MapIdx.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Mem.lean	chore: library style cleanup (#9654)	2025-07-31 21:28:59 +00:00
Monadic.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
OfFn.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Perm.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
QSort.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Range.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Set.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Subarray.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
TakeDrop.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Zip.lean	chore: remove grind annotations of List/Array/Vector.zip_map_left/right (#10163)	2025-08-28 10:38:50 +00:00