From cbe39dc4bb3c23b05ee00f649676bc8bb97ef757 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 26 Jul 2024 21:32:18 +1000 Subject: [PATCH] chore: fix List deprecations (#4842) --- src/Init/Data/List/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 29350a351d..5d18f52f6c 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1383,9 +1383,9 @@ theorem head_append {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) : theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all -@[deprecated append_ne_nil_of_ne_nil_left (since := "2024-07-24")] +@[deprecated append_ne_nil_of_left_ne_nil (since := "2024-07-24")] theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all -@[deprecated append_ne_nil_of_ne_nil_right (since := "2024-07-24")] +@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")] theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all theorem append_eq_cons :