Joachim Breitner 9deff2751f refactor: use reduceBEq in Init (#10398) ... This PR uses the `reduceBEq` simproc in Init, but mostly only for testing, because afer #10351 this code will be derived.		2025-09-16 10:35:46 +00:00
..
Basic.lean	feat: non-commutative ring normalizer in grind (#10375)	2025-09-14 07:35:08 +00:00
CommSemiringAdapter.lean	feat: non-commutative ring normalizer in grind (#10375)	2025-09-14 07:35:08 +00:00
CommSolver.lean	refactor: use reduceBEq in Init (#10398)	2025-09-16 10:35:46 +00:00
Envelope.lean	chore: replace Lean.Grind internal preorder classes with the classes from Std (#10129)	2025-08-26 13:18:22 +00:00
Field.lean	chore: remove a bad grind algebra instance (#10324)	2025-09-11 06:44:47 +00:00
ToInt.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00