chore: deprecation for Array.data

leanprover · Oct 13, 2024 · 68d6970 · 68d6970
1 parent 1d8555f
commit 68d6970
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
@@ -25,6 +25,8 @@ variable {α : Type u}
 
 namespace Array
 
+@[deprecated size (since := "2024-10-13")] abbrev data := @toList
+
 /-! ### Preliminary theorems -/
 
 @[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=