Leonardo de Moura 11f618ac49 feat: critical pairs (non commutative case) for grind ac (#10206) ... This PR adds superposition for associative (but non-commutative) operators in `grind ac`. Examples: ```lean example {α} (op : α → α → α) [Std.Associative op] (a b c d : α) : op a b = c → op b a = d → op (op c a) (op b c) = op (op a d) (op d b) := by grind example {α} (a b c d : List α) : a ++ b = c → b ++ a = d → c ++ a ++ b ++ c = a ++ d ++ d ++ b := by grind only ```		2025-09-02 00:58:49 +00:00
..
Module	chore: replace Lean.Grind internal preorder classes with the classes from Std (#10129)	2025-08-26 13:18:22 +00:00
Ordered	chore: replace Lean.Grind internal preorder classes with the classes from Std (#10129)	2025-08-26 13:18:22 +00:00
Ring	chore: replace Lean.Grind internal preorder classes with the classes from Std (#10129)	2025-08-26 13:18:22 +00:00
AC.lean	feat: critical pairs (non commutative case) for grind ac (#10206)	2025-09-02 00:58:49 +00:00
Attr.lean	doc: grind attribute modifiers (#10185)	2025-08-30 16:12:50 +00:00
Cases.lean	feat: attribute [grind cases eager] PProd MProd (#9121)	2025-07-01 04:02:47 +00:00
Ext.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Lemmas.lean	fix: equality congruence proofs in grind (#9767)	2025-08-06 16:40:27 +00:00
Module.lean	feat: add helper theorems for NatModule (#10069)	2025-08-22 20:36:05 +00:00
Norm.lean	chore: use SMul rather than HMul in grind algebra typeclasses (#10095)	2025-08-26 12:23:37 +00:00
Offset.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Ordered.lean	feat: upstream several Rat lemmas from mathlib (#10077)	2025-08-25 06:02:27 +00:00
PP.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Propagator.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Ring.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Tactics.lean	feat: simplify equations in grind AC module (#10165)	2025-08-28 03:54:09 +00:00
ToInt.lean	chore: add module keyword to grind tests (#10036)	2025-08-21 22:02:08 +00:00
ToIntLemmas.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Util.lean	refactor: module-ize remainder of Std (#9195)	2025-07-17 11:43:57 +00:00