| .. |
|
CommRing
|
fix: denotation functions for interfacing CommRing and linarith (#8693)
|
2025-06-09 14:43:13 +00:00 |
|
Module
|
feat: complete grind's ToInt framework (#8639)
|
2025-06-05 11:25:04 +00:00 |
|
Ordered
|
feat: model search procedure for grind linarith (#8690)
|
2025-06-09 04:31:28 +00:00 |
|
Cases.lean
|
fix: simplify isCasesAttrCandidate? in grind (#8415)
|
2025-05-20 14:29:07 +00:00 |
|
CommRing.lean
|
feat: draft typeclasses/tests for grind handling fields (#8417)
|
2025-05-20 13:44:11 +00:00 |
|
Ext.lean
|
fix: etaStruct and preprocessing issues in grind (#8344)
|
2025-05-15 03:32:10 +00:00 |
|
Lemmas.lean
|
fix: BEq support in grind (#8536)
|
2025-05-29 23:47:40 +00:00 |
|
Module.lean
|
feat: ordered ring typeclass for grind (#8429)
|
2025-05-21 07:05:01 +00:00 |
|
Norm.lean
|
feat: missing normalization rules in grind (#8413)
|
2025-05-20 02:38:29 +00:00 |
|
Offset.lean
|
feat: enable experimental module system in Init (#8047)
|
2025-04-23 17:21:33 +00:00 |
|
Ordered.lean
|
feat: background theorems for IntModule (#8637)
|
2025-06-05 02:32:53 +00:00 |
|
PP.lean
|
feat: enable experimental module system in Init (#8047)
|
2025-04-23 17:21:33 +00:00 |
|
Propagator.lean
|
feat: enable experimental module system in Init (#8047)
|
2025-04-23 17:21:33 +00:00 |
|
Tactics.lean
|
feat: proof term construction infrastructure for linarith in grind (#8687)
|
2025-06-08 19:58:48 +00:00 |
|
ToInt.lean
|
feat: complete grind's ToInt framework (#8639)
|
2025-06-05 11:25:04 +00:00 |
|
Util.lean
|
feat: generalized Option theorems for grind (#8572)
|
2025-06-01 06:25:37 +00:00 |
00f6b1e70a