fix: deprecations in Init.Data.Array.Basic (leanprover#5848)

opencompl · Oct 27, 2024 · ab9b5f4 · ab9b5f4
1 parent 81c977a
commit ab9b5f4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
@@ -25,7 +25,7 @@ variable {α : Type u}
 
 namespace Array
 
-@[deprecated size (since := "2024-10-13")] abbrev data := @toList
+@[deprecated toList (since := "2024-10-13")] abbrev data := @toList
 
 /-! ### Preliminary theorems -/
 
@@ -692,7 +692,7 @@ instance : HAppend (Array α) (List α) (Array α) := ⟨Array.appendList⟩
 def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
   as.foldlM (init := empty) fun bs a => do return bs ++ (← f a)
 
-@[deprecated concatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
+@[deprecated flatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
 
 @[inline]
 def flatMap (f : α → Array β) (as : Array α) : Array β :=