We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent bcec192 commit 9a2fe07Copy full SHA for 9a2fe07
tests/lean/run/grind_getElem.lean
@@ -6,5 +6,5 @@ attribute [grind]
6
List.getElem_cons
7
List.getElem?_cons List.getElem?_nil
8
9
-theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
+example {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
10
induction l generalizing i <;> grind
0 commit comments