| .. |
|
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: helper AC.Seq functions (#10164)
|
2025-08-28 02:16:52 +00:00 |
|
Attr.lean
|
feat: pattern inference using symbol priorities in grind (#9182)
|
2025-07-03 16:47:38 -07: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 |
38608a672e