Kim Morrison c06af84d9f fix: refactor grind's module/ring design to avoid a diamond (#9168) ... This PR resolves a defeq diamond, which caused a problem in Mathlib: ``` import Mathlib example (R : Type) [I : Ring R] : @AddCommGroup.toGrindIntModule R (@Ring.toAddCommGroup R I) = @Lean.Grind.Ring.instIntModule R (@Ring.toGrindRing R I) := rfl -- fails ```		2025-07-03 06:50:46 +00:00
..
Basic.lean	fix: refactor grind's module/ring design to avoid a diamond (#9168)	2025-07-03 06:50:46 +00:00
Envelope.lean	fix: refactor grind's module/ring design to avoid a diamond (#9168)	2025-07-03 06:50:46 +00:00