History

Kim Morrison 87152a3fae feat: `grind` annotations for `List.Sublist`/`IsInfix`/`IsPrefix`/`IsSuffix` (#8497 ) This PR adds preliminary grind annotations for `List.Sublist`/`IsInfix`/`IsPrefix`/`IsSuffix`, along with test cases.		2025-05-27 12:56:43 +00:00
..
experiments	chore: cleanup simp lemmas, following the simpNF linter (#8481 )	2025-05-26 04:13:17 +00:00
field_normalization.lean	feat: draft typeclasses/tests for grind handling fields (#8417 )	2025-05-20 13:44:11 +00:00
grind_palindrome.lean	chore: cleanup grind palindrome test (#8428 )	2025-05-21 03:31:56 +00:00
module_normalization.lean	chore: deduplicate Grind.RatModule and Grind.NoNatZeroDivisors (#8416 )	2025-05-20 07:49:42 +00:00
module_relations.lean	chore: deduplicate Grind.RatModule and Grind.NoNatZeroDivisors (#8416 )	2025-05-20 07:49:42 +00:00
ordered_modules.lean	chore: deduplicate Grind.RatModule and Grind.NoNatZeroDivisors (#8416 )	2025-05-20 07:49:42 +00:00
README.md
ring_normalization.lean	chore: add failing grind tests for noncommutative/non-negation rings (#8396 )	2025-05-19 00:26:16 +00:00
sublist.lean	feat: `grind` annotations for `List.Sublist`/`IsInfix`/`IsPrefix`/`IsSuffix` (#8497 )	2025-05-27 12:56:43 +00:00

Aspirational test cases for `grind`

These are not expected to work yet; we're collecting examples that we'd like to make work!

Aspirational test cases for grind