Leonardo de Moura 26138a5362 feat: equality propagation for comm ring procedure in grind (#8128) ... This PR implements equality propagation in the new commutative ring procedure in `grind`. The idea is to propagate implied equalities back to the `grind` core module that does congruence closure. In the following example, the equalities: `x^2*y = 1` and `x*y^2 - y = 0` imply that `y*x` is equal to `y*x*y`, which implies by congruence that `f (y*x) = f (y*x*y)`. ```lean example [CommRing α] (x y : α) (f : α → Nat) : x^2*y = 1 → x*y^2 - y = 0 → f (y*x) = f (y*x*y) := by grind +ring ```		2025-04-27 15:05:56 +00:00
..
ArgsPacker
Constructions
Match	chore: test that there are no orphaned modules (#8082)	2025-04-24 11:55:07 +00:00
Tactic	feat: equality propagation for comm ring procedure in grind (#8128)	2025-04-27 15:05:56 +00:00
AbstractMVars.lean
AbstractNestedProofs.lean	refactor: use mkAuxLemma in mkAuxTheorem (#7762)	2025-03-31 22:50:30 +00:00
ACLt.lean
AppBuilder.lean	feat: extract_lets and lift_lets tactics (#6432)	2025-04-21 08:57:01 +00:00
ArgsPacker.lean
Basic.lean	fix: missing traces from realizeConst (#8050)	2025-04-22 12:23:54 +00:00
BinderNameHint.lean	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
Canonicalizer.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Check.lean	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
CheckTactic.lean
Closure.lean	refactor: use mkAuxLemma in mkAuxTheorem (#7762)	2025-03-31 22:50:30 +00:00
Coe.lean	doc: docstring review for monads and transformers (#7548)	2025-03-20 12:18:46 +00:00
CoeAttr.lean
CollectFVars.lean
CollectMVars.lean
CompletionName.lean
CongrTheorems.lean	fix: transparency setting when computing congruence lemmas in grind (#7760)	2025-03-31 20:52:36 +00:00
Constructions.lean
CtorRecognizer.lean
DecLevel.lean
Diagnostics.lean
DiscrTree.lean
DiscrTreeTypes.lean
Eqns.lean	perf: remove more async blockers (#7497)	2025-03-15 11:07:04 +00:00
Eval.lean	perf: async optimizations for Init.Data.BitVec.Lemmas (#7546)	2025-03-18 12:56:16 +00:00
ExprDefEq.lean
ExprLens.lean
ExprTraverse.lean
ForEachExpr.lean
FunInfo.lean
GeneralizeTelescope.lean
GeneralizeVars.lean
GetUnfoldableConst.lean	perf: async optimizations for Init.Data.BitVec.Lemmas (#7546)	2025-03-18 12:56:16 +00:00
GlobalInstances.lean
IndPredBelow.lean	feat: deprecate Array.mkArray in favour of Array.replicate	2025-03-24 08:25:00 +01:00
Inductive.lean
InferType.lean	perf: Environment blocker removals from async-proofs branch (#7483)	2025-03-14 13:37:01 +00:00
Injective.lean
Instances.lean
IntInstTesters.lean
Iterator.lean
KAbstract.lean
KExprMap.lean
LazyDiscrTree.lean
LevelDefEq.lean
LitValues.lean	doc: Char docstring proofreading (#7198)	2025-03-08 22:17:01 +00:00
Match.lean
MatchUtil.lean
NatInstTesters.lean	feat: Nat divisibility constraints in cutsat (#7495)	2025-03-15 03:46:47 +00:00
Offset.lean
PPGoal.lean
PProdN.lean	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
RecursorInfo.lean
Reduce.lean
ReduceEval.lean
SizeOf.lean	feat: deprecate Array.mkArray in favour of Array.replicate	2025-03-24 08:25:00 +01:00
Sorry.lean
Structure.lean	refactor: factor out common code for structure default values (#7737)	2025-03-31 22:40:39 +00:00
SynthInstance.lean
Tactic.lean	feat: extract_lets and lift_lets tactics (#6432)	2025-04-21 08:57:01 +00:00
Transform.lean
TransparencyMode.lean
UnificationHint.lean
WHNF.lean	feat: zeta and zetaDelta options in grind (#7723)	2025-03-29 20:07:53 +00:00