From 82a26f4e5976fb131569822da782052ce92340ed Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sun, 13 Oct 2024 22:36:31 +1100
Subject: [PATCH] chore: deprecation for Array.data (#5687)

---
 src/Init/Data/Array/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 69418da8d64a..8f9ca1676be9 100644
--- 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 :=