From 38c39482f40536b864a9b43c718e10e8413b26e5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Oct 2024 16:37:36 +1100 Subject: [PATCH] chore: add missing deprecation dates (#5884) --- src/Init/Data/BitVec/Lemmas.lean | 2 +- src/Init/PropLemmas.lean | 4 ++-- src/Lean/Data/HashMap.lean | 12 ++++++------ src/Lean/Data/HashSet.lean | 10 +++++----- src/Lean/Meta/Tactic/Apply.lean | 2 +- src/Std/Data/HashMap/Basic.lean | 6 +++--- 6 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 950851505919..e1c7cb865863 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1792,7 +1792,7 @@ theorem setWidth_succ (x : BitVec w) : · simp_all · omega -@[deprecated "Use the reverse direction of `cons_msb_setWidth`"] +@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")] theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by simp diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index d9da88e596f3..f1ee950b88b1 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -643,11 +643,11 @@ theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop) (@ite _ p h q (decide p)) = (decide p && q) := by split <;> simp_all -@[deprecated ite_then_decide_self] +@[deprecated ite_then_decide_self (since := "2024-08-29")] theorem ite_true_decide_same (p : Prop) [Decidable p] (b : Bool) : (if p then decide p else b) = (decide p || b) := ite_then_decide_self p b -@[deprecated ite_false_decide_same] +@[deprecated ite_false_decide_same (since := "2024-08-29")] theorem ite_false_decide_same (p : Prop) [Decidable p] (b : Bool) : (if p then b else decide p) = (decide p && b) := ite_else_decide_self p b diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean index a8f975a98979..8899cb734665 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -271,11 +271,11 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β := | none => m.insert p.fst p.snd | some v => m.insert p.fst $ f v p.snd) -attribute [deprecated Std.HashMap] HashMap -attribute [deprecated Std.HashMap.Raw] HashMapImp -attribute [deprecated Std.HashMap.Raw.empty] mkHashMapImp -attribute [deprecated Std.HashMap.empty] mkHashMap -attribute [deprecated Std.HashMap.empty] HashMap.empty -attribute [deprecated Std.HashMap.ofList] HashMap.ofList +attribute [deprecated Std.HashMap (since := "2024-08-08")] HashMap +attribute [deprecated Std.HashMap.Raw (since := "2024-08-08")] HashMapImp +attribute [deprecated Std.HashMap.Raw.empty (since := "2024-08-08")] mkHashMapImp +attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] mkHashMap +attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] HashMap.empty +attribute [deprecated Std.HashMap.ofList (since := "2024-08-08")] HashMap.ofList end Lean.HashMap diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean index b7dc0cc09477..795566a3b5c7 100644 --- a/src/Lean/Data/HashSet.lean +++ b/src/Lean/Data/HashSet.lean @@ -219,8 +219,8 @@ def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α : t.fold (init := s) fun s a => s.insert a -- We don't use `insertMany` here because it gives weird universes. -attribute [deprecated Std.HashSet] HashSet -attribute [deprecated Std.HashSet.Raw] HashSetImp -attribute [deprecated Std.HashSet.Raw.empty] mkHashSetImp -attribute [deprecated Std.HashSet.empty] mkHashSet -attribute [deprecated Std.HashSet.empty] HashSet.empty +attribute [deprecated Std.HashSet (since := "2024-08-08")] HashSet +attribute [deprecated Std.HashSet.Raw (since := "2024-08-08")] HashSetImp +attribute [deprecated Std.HashSet.Raw.empty (since := "2024-08-08")] mkHashSetImp +attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] mkHashSet +attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] HashSet.empty diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index a292033c17e1..225424a5f3cd 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -254,7 +254,7 @@ Apply `And.intro` as much as possible to goal `mvarId`. abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) := splitAndCore mvarId -@[deprecated splitAnd] -- 2024-03-17 +@[deprecated splitAnd (since := "2024-03-17")] def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) := mvarId.splitAnd diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index 4a9afb333547..59fa81b39534 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -118,7 +118,7 @@ Tries to retrieve the mapping for the given key, returning `none` if no such map @[inline] def get? (m : HashMap α β) (a : α) : Option β := DHashMap.Const.get? m.inner a -@[deprecated get? "Use `m[a]?` or `m.get? a` instead", inherit_doc get?] +@[deprecated get? "Use `m[a]?` or `m.get? a` instead" (since := "2024-08-07"), inherit_doc get?] def find? (m : HashMap α β) (a : α) : Option β := m.get? a @@ -145,7 +145,7 @@ Retrieves the mapping for the given key. Ensures that such a mapping exists by r (fallback : β) : β := DHashMap.Const.getD m.inner a fallback -@[deprecated getD, inherit_doc getD] +@[deprecated getD (since := "2024-08-07"), inherit_doc getD] def findD (m : HashMap α β) (a : α) (fallback : β) : β := m.getD a fallback @@ -157,7 +157,7 @@ Tries to retrieve the mapping for the given key, panicking if no such mapping is @[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β := DHashMap.Const.get! m.inner a -@[deprecated get! "Use `m[a]!` or `m.get! a` instead", inherit_doc get!] +@[deprecated get! "Use `m[a]!` or `m.get! a` instead" (since := "2024-08-07"), inherit_doc get!] def find! [Inhabited β] (m : HashMap α β) (a : α) : Option β := m.get! a