Leonardo de Moura a3a11ffaf9 feat: revlex and grevlex monomial orders (#7986) ... This PR implements reverse lexicographical and graded reverse lexicographical orders for `CommRing` monomials.		2025-04-16 18:03:53 +00:00
..
CommRing	feat: revlex and grevlex monomial orders (#7986)	2025-04-16 18:03:53 +00:00
Cases.lean	feat: add [grind cases eager] Subtype (#7540)	2025-03-18 01:19:22 +00:00
CommRing.lean	feat: grind internal CommRing class (#7797)	2025-04-03 08:30:19 +00:00
Ext.lean	chore: add [grind ext] funext (#7951)	2025-04-14 02:52:44 +00:00
Lemmas.lean	feat: lookahead in grind (#7937)	2025-04-13 03:01:47 +00:00
Norm.lean	fix: mbtc and cast issue in grind (#7907)	2025-04-10 22:46:56 +00:00
Offset.lean	feat: literals, lower and upper bounds in the offset constraint module within grind (#6648)	2025-01-15 02:53:31 +00:00
PP.lean	feat: improve grind failure message (#6633)	2025-01-14 01:10:47 +00:00
Propagator.lean	feat: support for builtin grind propagators (#6448)	2024-12-25 22:55:39 +00:00
Tactics.lean	feat: add [grind ext] attribute (#7949)	2025-04-13 22:08:36 +00:00
Util.lean	feat: NatCast.natCast unexpander (#7775)	2025-04-01 17:11:44 +00:00