diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index c0d3bb9da773..6683bbab3f66 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 :=