chore: add missing since dates to deprecations (#875)

Batteries/Data/Array/Merge.lean

@@ -27,7 +27,7 @@ where
   termination_by xs.size + ys.size - (i + j)
 
 set_option linter.unusedVariables false in
-@[deprecated merge, inherit_doc merge]
+@[deprecated merge (since := "2024-04-24"), inherit_doc merge]
 def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α :=
   merge (compare · · |>.isLT) xs ys
 
@@ -55,7 +55,7 @@ where
       | .eq => go (acc.push (merge x y)) (i + 1) (j + 1)
   termination_by xs.size + ys.size - (i + j)
 
-@[deprecated] alias mergeSortedMergingDuplicates := mergeDedupWith
+@[deprecated (since := "2024-04-24")] alias mergeSortedMergingDuplicates := mergeDedupWith
 
 /--
 `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
@@ -64,7 +64,7 @@ not contain duplicates. If an element appears in both `xs` and `ys`, only one co
 @[inline] def mergeDedup [ord : Ord α] (xs ys : Array α) : Array α :=
   mergeDedupWith (ord := ord) xs ys fun x _ => x
 
-@[deprecated] alias mergeSortedDeduplicating := mergeDedup
+@[deprecated (since := "2024-04-24")] alias mergeSortedDeduplicating := mergeDedup
 
 set_option linter.unusedVariables false in
 /--
@@ -83,7 +83,7 @@ where
     ys.foldl (init := xs) fun xs y =>
       if xs.any (· == y) (stop := xsSize) then xs else xs.push y
 
-@[deprecated] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
+@[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
 
 /--
 `O(|xs|)`. Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with
@@ -101,7 +101,7 @@ where
       acc.push hd
   termination_by xs.size - i
 
-@[deprecated] alias mergeAdjacentDuplicates := mergeAdjacentDups
+@[deprecated (since := "2024-04-24")] alias mergeAdjacentDuplicates := mergeAdjacentDups
 
 /--
 `O(|xs|)`. Deduplicate a sorted array. The array must be sorted with to an order which agrees with
@@ -110,13 +110,13 @@ where
 def dedupSorted [eq : BEq α] (xs : Array α) : Array α :=
   xs.mergeAdjacentDups (eq := eq) fun x _ => x
 
-@[deprecated] alias deduplicateSorted := dedupSorted
+@[deprecated (since := "2024-04-24")] alias deduplicateSorted := dedupSorted
 
 /-- `O(|xs| log |xs|)`. Sort and deduplicate an array. -/
 def sortDedup [ord : Ord α] (xs : Array α) : Array α :=
   have := ord.toBEq
   dedupSorted <| xs.qsort (compare · · |>.isLT)
 
-@[deprecated] alias sortAndDeduplicate := sortDedup
+@[deprecated (since := "2024-04-24")] alias sortAndDeduplicate := sortDedup
 
 end Array

Batteries/Data/BitVec/Lemmas.lean

@@ -7,13 +7,10 @@ import Batteries.Tactic.Alias
 
 namespace BitVec
 
-/-- Replaced 2024-02-07. -/
-@[deprecated] alias zero_is_unique := eq_nil
+@[deprecated (since := "2024-02-07")] alias zero_is_unique := eq_nil
 
 /-! ### sub/neg -/
 
-/-- Replaced 2024-02-06. -/
-@[deprecated] alias sub_toNat := toNat_sub
+@[deprecated (since := "2024-02-07")] alias sub_toNat := toNat_sub
 
-/-- Replaced 2024-02-06. -/
-@[deprecated] alias neg_toNat := toNat_neg
+@[deprecated (since := "2024-02-07")] alias neg_toNat := toNat_neg

Batteries/Data/Bool.lean

@@ -10,10 +10,10 @@ namespace Bool
 
 /-! ### injectivity lemmas -/
 
-@[deprecated] alias not_inj' := not_inj_iff
+@[deprecated (since := "2023-10-27")] alias not_inj' := not_inj_iff
 
-@[deprecated] alias and_or_inj_right' := and_or_inj_right_iff
+@[deprecated (since := "2023-10-27")] alias and_or_inj_right' := and_or_inj_right_iff
 
-@[deprecated] alias and_or_inj_left' := and_or_inj_left_iff
+@[deprecated (since := "2023-10-27")] alias and_or_inj_left' := and_or_inj_left_iff
 
 end Bool

Batteries/Data/Int/Order.lean

@@ -7,4 +7,4 @@ import Batteries.Tactic.Alias
 
 namespace Int
 
-@[deprecated] alias ofNat_natAbs_eq_of_nonneg := natAbs_of_nonneg
+@[deprecated (since := "2024-01-24")] alias ofNat_natAbs_eq_of_nonneg := natAbs_of_nonneg

Batteries/Data/List/Basic.lean

@@ -93,9 +93,9 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
 /-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
 def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
 
-@[deprecated] alias removeNth := eraseIdx
-@[deprecated] alias removeNthTR := eraseIdxTR
-@[deprecated] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR
+@[deprecated (since := "2024-05-06")] alias removeNth := eraseIdx
+@[deprecated (since := "2024-05-06")] alias removeNthTR := eraseIdxTR
+@[deprecated (since := "2024-05-06")] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR
 
 /-- Replaces the first element of the list for which `f` returns `some` with the returned value. -/
 @[simp] def replaceF (f : α → Option α) : List α → List α
@@ -926,15 +926,15 @@ def range' : (start len : Nat) → (step : Nat := 1) → List Nat
 `ilast' x xs` returns the last element of `xs` if `xs` is non-empty; it returns `x` otherwise.
 Use `List.getLastD` instead.
 -/
-@[simp, deprecated getLastD] def ilast' {α} : α → List α → α
+@[simp, deprecated getLastD (since := "2024-01-09")] def ilast' {α} : α → List α → α
   | a, [] => a
   | _, b :: l => ilast' b l
 
 /--
 `last' xs` returns the last element of `xs` if `xs` is non-empty; it returns `none` otherwise.
 Use `List.getLast?` instead
 -/
-@[simp, deprecated getLast?] def last' {α} : List α → Option α
+@[simp, deprecated getLast? (since := "2024-01-09")] def last' {α} : List α → Option α
   | [] => none
   | [a] => some a
   | _ :: l => last' l

Batteries/Data/List/Count.lean

@@ -196,11 +196,11 @@ theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (coun
 theorem filter_eq (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
   filter_beq l a
 
-@[deprecated filter_eq]
+@[deprecated filter_eq (since := "2023-12-14")]
 theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
   simpa only [eq_comm] using filter_eq l a
 
-@[deprecated filter_beq]
+@[deprecated filter_beq (since := "2023-12-14")]
 theorem filter_beq' (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a := by
   simpa only [eq_comm (b := a)] using filter_eq l a
 

Batteries/Data/List/Lemmas.lean

@@ -308,7 +308,7 @@ theorem eraseIdx_eq_modifyNthTail : ∀ n (l : List α), eraseIdx l n = modifyNt
   | n+1, [] => rfl
   | n+1, a :: l => congrArg (cons _) (eraseIdx_eq_modifyNthTail _ _)
 
-@[deprecated] alias removeNth_eq_nth_tail := eraseIdx_eq_modifyNthTail
+@[deprecated (since := "2024-05-06")] alias removeNth_eq_nth_tail := eraseIdx_eq_modifyNthTail
 
 theorem getElem?_modifyNth (f : α → α) :
     ∀ n (l : List α) m, (modifyNth f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
@@ -472,7 +472,7 @@ theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i)
     simp [eraseIdx, ← Nat.add_one]
     rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
 
-@[deprecated] alias length_removeNth := length_eraseIdx
+@[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx
 
 /-! ### tail -/
 
@@ -619,7 +619,7 @@ theorem erase_subset (a : α) (l : List α) : l.erase a ⊆ l := (erase_sublist
 
 theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a := by
   simp only [erase_eq_eraseP']; exact h.eraseP
-@[deprecated] alias sublist.erase := Sublist.erase
+@[deprecated (since := "2024-04-22")] alias sublist.erase := Sublist.erase
 
 theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset _ _ h
 

Batteries/Data/List/Pairwise.lean

@@ -188,7 +188,7 @@ theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l 
         intro a b hab
         apply h; exact hab.cons _
 
-@[deprecated pairwise_iff_forall_sublist]
+@[deprecated pairwise_iff_forall_sublist (since := "2023-09-18")]
 theorem pairwise_of_reflexive_on_dupl_of_forall_ne [DecidableEq α] {l : List α} {r : α → α → Prop}
     (hr : ∀ a, 1 < count a l → r a a) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by
   apply pairwise_iff_forall_sublist.mpr

Batteries/Data/Nat/Lemmas.lean

@@ -151,19 +151,21 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
 
 /-! ## add -/
 
-@[deprecated] alias succ_add_eq_succ_add := Nat.succ_add_eq_add_succ
+@[deprecated (since := "2023-11-25")] alias succ_add_eq_succ_add := Nat.succ_add_eq_add_succ
 
 /-! ## sub -/
 
-@[deprecated] protected alias le_of_le_of_sub_le_sub_right := Nat.le_of_sub_le_sub_right
+@[deprecated (since := "2023-11-25")]
+protected alias le_of_le_of_sub_le_sub_right := Nat.le_of_sub_le_sub_right
 
-@[deprecated] protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left
+@[deprecated (since := "2023-11-25")]
+protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left
 
 /-! ### mul -/
 
-@[deprecated] protected alias mul_lt_mul := Nat.mul_lt_mul_of_lt_of_le'
+@[deprecated (since := "2024-01-11")] protected alias mul_lt_mul := Nat.mul_lt_mul_of_lt_of_le'
 
-@[deprecated] protected alias mul_lt_mul' := Nat.mul_lt_mul_of_le_of_lt
+@[deprecated (since := "2024-01-11")] protected alias mul_lt_mul' := Nat.mul_lt_mul_of_le_of_lt
 
 /-! ### div/mod -/
 
@@ -182,5 +184,5 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
 @[simp] theorem sum_append : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂ := by
   induction l₁ <;> simp [*, Nat.add_assoc]
 
-@[deprecated] protected alias lt_connex := Nat.lt_or_gt_of_ne
-@[deprecated] alias pow_two_pos := Nat.two_pow_pos -- deprecated 2024-02-09
+@[deprecated (since := "2024-03-05")] protected alias lt_connex := Nat.lt_or_gt_of_ne
+@[deprecated (since := "2024-02-09")] alias pow_two_pos := Nat.two_pow_pos

Batteries/Data/Option/Lemmas.lean

@@ -7,7 +7,7 @@ import Batteries.Tactic.Alias
 
 namespace Option
 
-@[deprecated] alias to_list_some := toList_some
-@[deprecated] alias to_list_none := toList_none
+@[deprecated (since := "2024-03-05")] alias to_list_some := toList_some
+@[deprecated (since := "2024-03-05")] alias to_list_none := toList_none
 
 end Option

Batteries/Data/RBMap/Basic.lean

@@ -67,8 +67,8 @@ protected def max? : RBNode α → Option α
   | node _ _ v nil => some v
   | node _ _ _ r   => r.max?
 
-@[deprecated] protected alias min := RBNode.min?
-@[deprecated] protected alias max := RBNode.max?
+@[deprecated (since := "2024-04-17")] protected alias min := RBNode.min?
+@[deprecated (since := "2024-04-17")] protected alias max := RBNode.max?
 
 /--
 Fold a function in tree order along the nodes. `v₀` is used at `nil` nodes and
@@ -669,8 +669,8 @@ instance : ToStream (RBSet α cmp) (RBNode.Stream α) := ⟨fun x => x.1.toStrea
 /-- `O(log n)`. Returns the entry `a` such that `a ≥ k` for all keys in the RBSet. -/
 @[inline] protected def max? (t : RBSet α cmp) : Option α := t.1.max?
 
-@[deprecated] protected alias min := RBSet.min?
-@[deprecated] protected alias max := RBSet.max?
+@[deprecated (since := "2024-04-17")] protected alias min := RBSet.min?
+@[deprecated (since := "2024-04-17")] protected alias max := RBSet.max?
 
 instance [Repr α] : Repr (RBSet α cmp) where
   reprPrec m prec := Repr.addAppParen ("RBSet.ofList " ++ repr m.toList) prec
@@ -1053,8 +1053,8 @@ instance : Stream (Values.Stream α β) β := ⟨Values.Stream.next?⟩
 /-- `O(log n)`. Returns the key-value pair `(a, b)` such that `a ≥ k` for all keys in the RBMap. -/
 @[inline] protected def max? : RBMap α β cmp → Option (α × β) := RBSet.max?
 
-@[deprecated] protected alias min := RBMap.min?
-@[deprecated] protected alias max := RBMap.max?
+@[deprecated (since := "2024-04-17")] protected alias min := RBMap.min?
+@[deprecated (since := "2024-04-17")] protected alias max := RBMap.max?
 
 instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
   reprPrec m prec := Repr.addAppParen ("RBMap.ofList " ++ repr m.toList) prec

Batteries/Lean/Delaborator.lean

@@ -8,6 +8,6 @@ import Lean.PrettyPrinter
 open Lean PrettyPrinter Delaborator SubExpr
 
 /-- Abbreviation for `Lean.MessageData.ofConst`. -/
-@[deprecated Lean.MessageData.ofConst]
+@[deprecated Lean.MessageData.ofConst (since := "2024-05-18")]
 def Lean.ppConst (e : Expr) : MessageData :=
   Lean.MessageData.ofConst e

Batteries/Logic.lean

@@ -10,7 +10,7 @@ import Batteries.Tactic.Lint.Misc
 instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) :=
   inferInstanceAs <| DecidablePred fun x => p (f x)
 
-@[deprecated] alias proofIrrel := proof_irrel
+@[deprecated (since := "2024-03-15")] alias proofIrrel := proof_irrel
 
 /-! ## id -/
 

Batteries/StdDeprecations.lean

@@ -21,35 +21,36 @@ but it would be much harder to generate the deprecations.
 Let's hope that people using the tactic implementations can work this out themselves.
 -/
 
-@[deprecated] alias Std.AssocList := Batteries.AssocList
-@[deprecated] alias Std.HashMap := Batteries.HashMap
-@[deprecated] alias Std.mkHashMap := Batteries.mkHashMap
-@[deprecated] alias Std.DList := Batteries.DList
-@[deprecated] alias Std.PairingHeapImp.Heap := Batteries.PairingHeapImp.Heap
-@[deprecated] alias Std.TotalBLE := Batteries.TotalBLE
-@[deprecated] alias Std.OrientedCmp := Batteries.OrientedCmp
-@[deprecated] alias Std.TransCmp := Batteries.TransCmp
-@[deprecated] alias Std.BEqCmp := Batteries.BEqCmp
-@[deprecated] alias Std.LTCmp := Batteries.LTCmp
-@[deprecated] alias Std.LECmp := Batteries.LECmp
-@[deprecated] alias Std.LawfulCmp := Batteries.LawfulCmp
-@[deprecated] alias Std.OrientedOrd := Batteries.OrientedOrd
-@[deprecated] alias Std.TransOrd := Batteries.TransOrd
-@[deprecated] alias Std.BEqOrd := Batteries.BEqOrd
-@[deprecated] alias Std.LTOrd := Batteries.LTOrd
-@[deprecated] alias Std.LEOrd := Batteries.LEOrd
-@[deprecated] alias Std.LawfulOrd := Batteries.LawfulOrd
-@[deprecated] alias Std.compareOfLessAndEq_eq_lt := Batteries.compareOfLessAndEq_eq_lt
-@[deprecated] alias Std.RBColor := Batteries.RBColor
-@[deprecated] alias Std.RBNode := Batteries.RBNode
-@[deprecated] alias Std.RBSet := Batteries.RBSet
-@[deprecated] alias Std.mkRBSet := Batteries.mkRBSet
-@[deprecated] alias Std.RBMap := Batteries.RBMap
-@[deprecated] alias Std.mkRBMap := Batteries.mkRBMap
-@[deprecated] alias Std.BinomialHeap := Batteries.BinomialHeap
-@[deprecated] alias Std.mkBinomialHeap := Batteries.mkBinomialHeap
-@[deprecated] alias Std.UFNode := Batteries.UFNode
-@[deprecated] alias Std.UnionFind := Batteries.UnionFind
+@[deprecated (since := "2024-05-07")] alias Std.AssocList := Batteries.AssocList
+@[deprecated (since := "2024-05-07")] alias Std.HashMap := Batteries.HashMap
+@[deprecated (since := "2024-05-07")] alias Std.mkHashMap := Batteries.mkHashMap
+@[deprecated (since := "2024-05-07")] alias Std.DList := Batteries.DList
+@[deprecated (since := "2024-05-07")] alias Std.PairingHeapImp.Heap := Batteries.PairingHeapImp.Heap
+@[deprecated (since := "2024-05-07")] alias Std.TotalBLE := Batteries.TotalBLE
+@[deprecated (since := "2024-05-07")] alias Std.OrientedCmp := Batteries.OrientedCmp
+@[deprecated (since := "2024-05-07")] alias Std.TransCmp := Batteries.TransCmp
+@[deprecated (since := "2024-05-07")] alias Std.BEqCmp := Batteries.BEqCmp
+@[deprecated (since := "2024-05-07")] alias Std.LTCmp := Batteries.LTCmp
+@[deprecated (since := "2024-05-07")] alias Std.LECmp := Batteries.LECmp
+@[deprecated (since := "2024-05-07")] alias Std.LawfulCmp := Batteries.LawfulCmp
+@[deprecated (since := "2024-05-07")] alias Std.OrientedOrd := Batteries.OrientedOrd
+@[deprecated (since := "2024-05-07")] alias Std.TransOrd := Batteries.TransOrd
+@[deprecated (since := "2024-05-07")] alias Std.BEqOrd := Batteries.BEqOrd
+@[deprecated (since := "2024-05-07")] alias Std.LTOrd := Batteries.LTOrd
+@[deprecated (since := "2024-05-07")] alias Std.LEOrd := Batteries.LEOrd
+@[deprecated (since := "2024-05-07")] alias Std.LawfulOrd := Batteries.LawfulOrd
+@[deprecated (since := "2024-05-07")]
+alias Std.compareOfLessAndEq_eq_lt := Batteries.compareOfLessAndEq_eq_lt
+@[deprecated (since := "2024-05-07")] alias Std.RBColor := Batteries.RBColor
+@[deprecated (since := "2024-05-07")] alias Std.RBNode := Batteries.RBNode
+@[deprecated (since := "2024-05-07")] alias Std.RBSet := Batteries.RBSet
+@[deprecated (since := "2024-05-07")] alias Std.mkRBSet := Batteries.mkRBSet
+@[deprecated (since := "2024-05-07")] alias Std.RBMap := Batteries.RBMap
+@[deprecated (since := "2024-05-07")] alias Std.mkRBMap := Batteries.mkRBMap
+@[deprecated (since := "2024-05-07")] alias Std.BinomialHeap := Batteries.BinomialHeap
+@[deprecated (since := "2024-05-07")] alias Std.mkBinomialHeap := Batteries.mkBinomialHeap
+@[deprecated (since := "2024-05-07")] alias Std.UFNode := Batteries.UFNode
+@[deprecated (since := "2024-05-07")] alias Std.UnionFind := Batteries.UnionFind
 
 -- Check that these generate usable deprecated hints
 -- when referring to names inside these namespaces.