2979830120
This PR adds a new propagation rule for `Bool` disequalities to `grind`. It now propagates `x = true` (`x = false`) from the disequality `x = false` (`x = true`). It ensures we don't have to perform case analysis on `x` to learn this fact. See tests. |
||
|---|---|---|
| .. | ||
| clear_aux_decls.lean | ||
| model_conjectures.lean | ||
| README.md | ||
Aspirational test cases for grind
These are not expected to work yet; we're collecting examples that we'd like to make work!