Commit 2025-07-02 12:44 eeb88358

View on Github →

chore: use grind instead of cc (#26194) This PR removes uses of cc in Mathlib, replacing them with grind. It also adds some grind test cases derived from the test cases for cc. Note that there are cc test cases which grind can not (and will not; by design avoiding higher order unification) solve, but there is nothing in the library itself that uses these capabilities.

Estimated changes