chore: remove duplicate theorem about lists (#986)

leanprover-community · Oct 14, 2024 · 5f963d5 · 5f963d5
1 parent 9efd9c2
commit 5f963d5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
@@ -17,7 +17,7 @@ namespace List
 
 /-! ### isEmpty -/
 
-theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty]
+@[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
 
 /-! ### next? -/