Leonardo de Moura dac61c406f feat: extra critical pairs for associative + idempotent operators in grind ac (#10221) ... This PR adds the extra critical pairs to ensure the `grind ac` procedure is complete when the operator is associative and idempotent, but not commutative. Example: ```lean example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.IdempotentOp op] (a b c d e f x y w : α) : op d (op x c) = op a b → op e (op f (op y w)) = op a (op b c) → op d (op x c) = op e (op f (op y w)) := by grind only example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.IdempotentOp op] (a b c d e f x y w : α) : op a (op d x) = op b c → op e (op f (op y w)) = op a (op b c) → op a (op d x) = op e (op f (op y w)) := by grind only ```		2025-09-02 15:52:56 +00:00
..
bench	chore: fix stdlib size benchmarks	2025-08-28 12:07:27 +02:00
compiler	fix: Unicode path support for Lean Windows executables (#10133)	2025-08-27 11:28:55 +00:00
elabissues
ir
lean	feat: extra critical pairs for associative + idempotent operators in grind ac (#10221)	2025-09-02 15:52:56 +00:00
pkg	chore: improve error message on trying to access an identifier imported privately from the public scope (#10153)	2025-08-27 13:43:56 +00:00
playground	chore: eliminate uses of intros x y z (#9983)	2025-08-19 06:09:13 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain