History

Leonardo de Moura ba1c1258d7 feat: case split on implications in `grind` (#7864 ) This PR adds support to `grind` for case splitting on implications of the form `p -> q` and `(h : p) -> q h`. See the new option `(splitImp := true)`.		2025-04-08 00:10:43 +00:00
..
clear_aux_decls.lean
list_problems.lean	feat: case split on implications in `grind` (#7864 )	2025-04-08 00:10:43 +00:00
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!

Aspirational test cases for grind