264095be7f
This PR fixes two issues that were preventing `grind` to solve `getElem?_eq_some_iff`. 1. Missing propagation rule for `Exists p = False` 2. Missing conditions at `isCongrToPrevSplit` a filter for discarding unnecessary case-splits.
10 lines
277 B
Text
10 lines
277 B
Text
reset_grind_attrs%
|
||
|
||
attribute [grind] List.getElem_append_left List.getElem_append_right
|
||
attribute [grind] List.length_cons List.length_nil
|
||
|
||
example {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
|
||
(l ++ [a])[i]'w = a := by
|
||
grind -- Similar to issue above.
|
||
|
||
---
|