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.