32eedc2c22
This PR adds an option for disabling the cutsat procedure in `grind`. The linarith module takes over linear integer/nat constraints. Example: ```lean set_option trace.grind.cutsat.assert true in -- cutsat should **not** process the following constraints example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12*y - 4* z < 0 := by grind -cutsat -- `linarith` module solves it ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||