From 18f8a18bfcadfce98d4285deeaba97cdc53cfef1 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 26 Apr 2025 23:10:05 +1000 Subject: [PATCH] chore: fix TreeMap deprecations (#8100) This PR fixes some incorrect deprecations in TreeMap. --- src/Std/Data/TreeMap/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean index 177becd389..2e1a1ea8aa 100644 --- a/src/Std/Data/TreeMap/Basic.lean +++ b/src/Std/Data/TreeMap/Basic.lean @@ -216,7 +216,7 @@ def minD (t : TreeMap α β cmp) (fallback : α × β) : α × β := def maxEntry? (t : TreeMap α β cmp) : Option (α × β) := DTreeMap.Const.maxEntry? t.inner -@[inline, inherit_doc maxEntry?, deprecated minEntry? (since := "2025-03-13")] +@[inline, inherit_doc maxEntry?, deprecated maxEntry? (since := "2025-03-13")] def max? (t : TreeMap α β cmp) : Option (α × β) := t.maxEntry? @@ -224,7 +224,7 @@ def max? (t : TreeMap α β cmp) : Option (α × β) := def maxEntry (t : TreeMap α β cmp) (h : t.isEmpty = false) : α × β := DTreeMap.Const.maxEntry t.inner h -@[inline, inherit_doc maxEntry, deprecated minEntry (since := "2025-03-13")] +@[inline, inherit_doc maxEntry, deprecated maxEntry (since := "2025-03-13")] def max (t : TreeMap α β cmp) (h : t.isEmpty = false) : α × β := t.maxEntry h @@ -232,7 +232,7 @@ def max (t : TreeMap α β cmp) (h : t.isEmpty = false) : α × β := def maxEntry! [Inhabited (α × β)] (t : TreeMap α β cmp) : α × β := DTreeMap.Const.maxEntry! t.inner -@[inline, inherit_doc maxEntry!, deprecated minEntry! (since := "2025-03-13")] +@[inline, inherit_doc maxEntry!, deprecated maxEntry! (since := "2025-03-13")] def max! [Inhabited (α × β)] (t : TreeMap α β cmp) : α × β := t.maxEntry! @@ -240,7 +240,7 @@ def max! [Inhabited (α × β)] (t : TreeMap α β cmp) : α × β := def maxEntryD (t : TreeMap α β cmp) (fallback : α × β) : α × β := DTreeMap.Const.maxEntryD t.inner fallback -@[inline, inherit_doc maxEntryD, deprecated minEntryD (since := "2025-03-13")] +@[inline, inherit_doc maxEntryD, deprecated maxEntryD (since := "2025-03-13")] def maxD (t : TreeMap α β cmp) (fallback : α × β) : α × β := t.maxEntryD fallback