Skip to content

Commit bf0bc78

Browse files
committed
unsimp List.getElem?_length
This is solved using `getElem?_neg` now.
1 parent ebdb211 commit bf0bc78

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

Mathlib/Data/List/Basic.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -590,7 +590,6 @@ end IndexOf
590590

591591
section deprecated
592592

593-
@[simp]
594593
theorem getElem?_length (l : List α) : l[l.length]? = none := getElem?_eq_none le_rfl
595594

596595
/-- A version of `getElem_map` that can be used for rewriting. -/

0 commit comments

Comments
 (0)