Init.Data.Array.Bootstrap

Array.get definition

{α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α

Full source

/--
Use the indexing notation `a[i]` instead.

Access an element from an array without needing a runtime bounds checks,
using a `Nat` index and a proof that it is in bounds.

This function does not use `get_elem_tactic` to automatically find the proof that
the index is in bounds. This is because the tactic itself needs to look up values in
arrays.
-/
@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
def get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
  a.toList.get ⟨i, h⟩

Array element access with proof of bounds

Informal description

Given an array `a` of type `α`, a natural number index `i`, and a proof `h` that `i` is less than the size of `a`, the function returns the element at position `i` in the array. This function avoids runtime bounds checks by requiring a proof that the index is valid.

Array.get! definition

{α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α

Full source

/--
Use the indexing notation `a[i]!` instead.

Access an element from an array, or panic if the index is out of bounds.
-/
@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17")]
def get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
  Array.getD a i default

Array element access with default fallback

Informal description

Given an array $a$ of type $\alpha$ (where $\alpha$ is an inhabited type) and a natural number index $i$, the function returns the element at position $i$ in $a$ if $i$ is within bounds (i.e., $0 \leq i < \text{size}(a)$), and returns the default value of $\alpha$ otherwise.

Array.foldlM_toList.aux theorem

 [Monad m] {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :
  foldlM.loop f xs xs.size (Nat.le_refl _) i j b = (xs.toList.drop j).foldlM f b

Full source

theorem foldlM_toList.aux [Monad m]
    {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :
    foldlM.loop f xs xs.size (Nat.le_refl _) i j b = (xs.toList.drop j).foldlM f b := by
  unfold foldlM.loop
  split; split
  · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
  · rename_i i; rw [Nat.succ_add] at H
    simp [foldlM_toList.aux (j := j+1) H]
    rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
    rfl
  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl

Equality of Monadic Folds on Array and Dropped List

Informal description

Let $m$ be a monad, $f : \beta \to \alpha \to m \beta$ a function, $xs$ an array of elements of type $\alpha$, and $i, j$ natural numbers such that the size of $xs$ is at most $i + j$. Then for any initial value $b : \beta$, the monadic fold operation `foldlM.loop` applied to $f$, $xs$, its size, and indices $i, j$ with $b$ is equal to the monadic fold operation applied to $f$ and $b$ over the list obtained by dropping the first $j$ elements from the list representation of $xs$.

Array.foldlM_toList theorem

[Monad m] {f : β → α → m β} {init : β} {xs : Array α} : xs.toList.foldlM f init = xs.foldlM f init

Full source

@[simp] theorem foldlM_toList [Monad m]
    {f : β → α → m β} {init : β} {xs : Array α} :
    xs.toList.foldlM f init = xs.foldlM f init := by
  simp [foldlM, foldlM_toList.aux]

Equality of Monadic Left Folds on Array and Its List Representation

Informal description

Let $m$ be a monad, $f : \beta \to \alpha \to m \beta$ a function, and $xs$ an array of elements of type $\alpha$. For any initial value $init : \beta$, the monadic left fold operation applied to $f$ and $init$ over the list representation of $xs$ is equal to the monadic left fold operation applied to $f$ and $init$ over the array $xs$ itself.

Array.foldl_toList theorem

(f : β → α → β) {init : β} {xs : Array α} : xs.toList.foldl f init = xs.foldl f init

Full source

@[simp] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} :
    xs.toList.foldl f init = xs.foldl f init :=
  List.foldl_eq_foldlM .. ▸ foldlM_toList ..

Equality of Left Folds on Array and Its List Representation

Informal description

For any binary operation $f : \beta \to \alpha \to \beta$, initial value $init : \beta$, and array $xs$ of elements of type $\alpha$, the left fold of $f$ over the list representation of $xs$ with initial value $init$ is equal to the left fold of $f$ over the array $xs$ itself with the same initial value.

Array.foldrM_eq_reverse_foldlM_toList.aux theorem

 [Monad m] {f : α → β → m β} {xs : Array α} {init : β} {i} (h) :
  (xs.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f xs 0 i h init

Full source

theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
    {f : α → β → m β} {xs : Array α} {init : β} {i} (h) :
    (xs.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f xs 0 i h init := by
  unfold foldrM.fold
  match i with
  | 0 => simp [List.foldlM, List.take]
  | i+1 => rw [← List.take_concat_get h]; simp [← aux]

Equivalence of Monadic Left Fold on Reversed Prefix and Auxiliary Right Fold for Arrays

Informal description

Let $m$ be a monad, $f : \alpha \to \beta \to m \beta$ a function, $xs$ an array of type $\alpha$, $init$ an element of type $\beta$, and $i$ a natural number such that $h$ holds. Then the monadic left fold of the reversed first $i$ elements of $xs$ (converted to a list) with function $\lambda x y, f y x$ and initial value $init$ is equal to the auxiliary monadic right fold operation applied to $f$, $xs$, $0$, $i$, $h$, and $init$.

Array.foldrM_eq_reverse_foldlM_toList theorem

 [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
  xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init

Full source

theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
    xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by
  have : xs = #[] ∨ 0 < xs.size :=
    match xs with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
  match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_
  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]

Equivalence of Monadic Right Fold on Arrays and Left Fold on Reversed Lists

Informal description

Let $m$ be a monad, $f : \alpha \to \beta \to m \beta$ a function, $init$ an element of type $\beta$, and $xs$ an array of type $\alpha$. Then the monadic right fold of $xs$ with function $f$ and initial value $init$ is equal to the monadic left fold of the reversed list representation of $xs$ with the flipped function $\lambda x y, f y x$ and initial value $init$.

Array.foldrM_toList theorem

[Monad m] {f : α → β → m β} {init : β} {xs : Array α} : xs.toList.foldrM f init = xs.foldrM f init

Full source

@[simp] theorem foldrM_toList [Monad m]
    {f : α → β → m β} {init : β} {xs : Array α} :
    xs.toList.foldrM f init = xs.foldrM f init := by
  rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]

Equivalence of Monadic Right Folds on Array and its List Representation

Informal description

Let $m$ be a monad, $f : \alpha \to \beta \to m \beta$ a function, $init$ an element of type $\beta$, and $xs$ an array of type $\alpha$. Then the monadic right fold of the list representation of $xs$ with function $f$ and initial value $init$ is equal to the monadic right fold of $xs$ with the same function and initial value.

Array.foldr_toList theorem

(f : α → β → β) {init : β} {xs : Array α} : xs.toList.foldr f init = xs.foldr f init

Full source

@[simp] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} :
    xs.toList.foldr f init = xs.foldr f init :=
  List.foldr_eq_foldrM .. ▸ foldrM_toList ..

Equivalence of Right Folds on Array and its List Representation

Informal description

For any function $f : \alpha \to \beta \to \beta$, initial value $init : \beta$, and array $xs : \text{Array } \alpha$, the right fold of the list representation of $xs$ with function $f$ and initial value $init$ is equal to the right fold of $xs$ with the same function and initial value. That is, $\text{foldr } f \text{ init } (xs.\text{toList}) = xs.\text{foldr } f \text{ init}$.

Array.push_toList theorem

{xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a]

Full source

@[simp] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
  simp [push, List.concat_eq_append]

Conversion of Pushed Array to List Equals List Append

Informal description

For any array `xs` of type `Array α` and any element `a` of type `α`, converting the array `xs.push a` (obtained by appending `a` to `xs`) to a list yields the same result as appending the singleton list `[a]` to the list obtained by converting `xs` to a list. In other words, `(xs.push a).toList = xs.toList ++ [a]`.

Array.toListAppend_eq theorem

{xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l

Full source

@[simp] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
  simp [toListAppend, ← foldr_toList]

List Conversion with Append Preserves Concatenation

Informal description

For any array `xs` of type `Array α` and any list `l` of type `List α`, the result of `xs.toListAppend l` is equal to the concatenation of `xs.toList` and `l`, i.e., `xs.toList ++ l`.

Array.toListImpl_eq theorem

{xs : Array α} : xs.toListImpl = xs.toList

Full source

@[simp] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by
  simp [toListImpl, ← foldr_toList]

Equivalence of Internal and Standard Array-to-List Conversions

Informal description

For any array `xs` of type `Array α`, the result of the internal list conversion function `toListImpl` is equal to the standard list conversion `toList`, i.e., `xs.toListImpl = xs.toList`.

Array.toList_pop theorem

{xs : Array α} : xs.pop.toList = xs.toList.dropLast

Full source

@[simp] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl

List Conversion Preserves Array Pop Operation

Informal description

For any array `xs` of type `Array α`, the list obtained by converting the array after removing its last element (`xs.pop.toList`) is equal to the list obtained by converting the original array (`xs.toList`) with its last element removed (`dropLast`).

Array.pop_toList abbrev

Full source

@[deprecated toList_pop (since := "2025-02-17")]
abbrev pop_toList := @Array.toList_pop

List Conversion Preserves Array Pop Operation

Informal description

For any array `xs` of type `Array α`, the list obtained by converting the array after removing its last element (`xs.pop.toList`) is equal to the list obtained by converting the original array (`xs.toList`) with its last element removed (`dropLast`).

Array.append_eq_append theorem

{xs ys : Array α} : xs.append ys = xs ++ ys

Full source

@[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl

Equivalence of Array Append Operations: `xs.append ys = xs ++ ys`

Informal description

For any arrays `xs` and `ys` of type `Array α`, the result of the `append` operation on `xs` and `ys` is equal to the result of the `++` operation on `xs` and `ys`.

Array.toList_append theorem

{xs ys : Array α} : (xs ++ ys).toList = xs.toList ++ ys.toList

Full source

@[simp] theorem toList_append {xs ys : Array α} :
    (xs ++ ys).toList = xs.toList ++ ys.toList := by
  rw [← append_eq_append]; unfold Array.append
  rw [← foldl_toList]
  induction ys.toList generalizing xs <;> simp [*]

List Conversion Preserves Array Concatenation

Informal description

For any arrays `xs` and `ys` of type `Array α`, converting the concatenated array `xs ++ ys` to a list yields the same result as concatenating the list representations of `xs` and `ys`. That is, $(xs ++ ys).\text{toList} = xs.\text{toList} ++ ys.\text{toList}$.

Array.toList_empty theorem

: (#[] : Array α).toList = []

Full source

@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl

Empty Array to List Conversion Yields Empty List

Informal description

The conversion of an empty array `#[]` of type `Array α` to a list results in the empty list `[]`.

Array.append_empty theorem

{xs : Array α} : xs ++ #[] = xs

Full source

@[simp] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
  apply ext'; simp only [toList_append, toList_empty, List.append_nil]

Right Concatenation with Empty Array Preserves Identity

Informal description

For any array `xs` of type `Array α`, concatenating `xs` with the empty array `#[]` yields `xs` itself, i.e., `xs ++ #[] = xs`.

Array.append_nil abbrev

Full source

@[deprecated append_empty (since := "2025-01-13")]
abbrev append_nil := @append_empty

Right Identity of Array Concatenation with Empty Array

Informal description

For any array `xs` of type `Array α`, concatenating `xs` with the empty array `#[]` yields `xs` itself, i.e., `xs ++ #[] = xs`.

Array.empty_append theorem

{xs : Array α} : #[] ++ xs = xs

Full source

@[simp] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
  apply ext'; simp only [toList_append, toList_empty, List.nil_append]

Left Identity of Array Concatenation with Empty Array

Informal description

For any array `xs` of type `Array α`, concatenating the empty array `#[]` with `xs` yields `xs`, i.e., `#[] ++ xs = xs`.

Array.nil_append abbrev

Full source

@[deprecated empty_append (since := "2025-01-13")]
abbrev nil_append := @empty_append

Right Identity of Array Concatenation with Empty Array

Informal description

For any array `xs` of type `Array α`, concatenating `xs` with the empty array `#[]` yields `xs`, i.e., `xs ++ #[] = xs`.

Array.append_assoc theorem

{xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs)

Full source

@[simp] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
  apply ext'; simp only [toList_append, List.append_assoc]

Associativity of Array Concatenation: $(xs \mathbin{+\!\!+} ys) \mathbin{+\!\!+} zs = xs \mathbin{+\!\!+} (ys \mathbin{+\!\!+} zs)$

Informal description

For any arrays $xs$, $ys$, and $zs$ of type $\text{Array}\,\alpha$, the concatenation operation is associative, i.e., $(xs \mathbin{+\!\!+} ys) \mathbin{+\!\!+} zs = xs \mathbin{+\!\!+} (ys \mathbin{+\!\!+} zs)$.

Array.appendList_eq_append theorem

{xs : Array α} {l : List α} : xs.appendList l = xs ++ l

Full source

@[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl

Equivalence of Array AppendList and Concatenation

Informal description

For any array `xs` of type `Array α` and any list `l` of type `List α`, the operation `xs.appendList l` is equal to the concatenation `xs ++ l`.

Array.toList_appendList theorem

{xs : Array α} {l : List α} : (xs ++ l).toList = xs.toList ++ l

Full source

@[simp] theorem toList_appendList {xs : Array α} {l : List α} :
    (xs ++ l).toList = xs.toList ++ l := by
  rw [← appendList_eq_append]; unfold Array.appendList
  induction l generalizing xs <;> simp [*]

List Conversion Preserves Array Concatenation

Informal description

For any array `xs` of type `Array α` and any list `l` of type `List α`, converting the concatenated array `xs ++ l` to a list yields the same result as concatenating the list conversion of `xs` with `l`. In other words, $(xs \mathbin{+\!\!+} l).\text{toList} = xs.\text{toList} \mathbin{+\!\!+} l$.

Array.appendList_toList abbrev

Full source

@[deprecated toList_appendList (since := "2024-12-11")]
abbrev appendList_toList := @toList_appendList

List Conversion Preserves Array AppendList Operation

Informal description

For any array `xs` of type `Array α` and any list `l` of type `List α`, converting the array `xs.appendList l` to a list yields the same result as concatenating the list conversion of `xs` with `l`. In other words, $(xs.\text{appendList} l).\text{toList} = xs.\text{toList} \mathbin{+\!\!+} l$.

Array.foldrM_eq_foldrM_toList theorem

[Monad m] {f : α → β → m β} {init : β} {xs : Array α} : xs.foldrM f init = xs.toList.foldrM f init

Full source

@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
theorem foldrM_eq_foldrM_toList [Monad m]
    {f : α → β → m β} {init : β} {xs : Array α} :
    xs.foldrM f init = xs.toList.foldrM f init := by
  simp

Equality of Monadic Right Folds on Array and Its List Representation

Informal description

Let $m$ be a monad, $f : \alpha \to \beta \to m \beta$ a function, and $xs$ an array of elements of type $\alpha$. For any initial value $init : \beta$, the monadic right fold operation applied to $f$ and $init$ over the array $xs$ is equal to the monadic right fold operation applied to $f$ and $init$ over the list representation of $xs$.

Array.foldlM_eq_foldlM_toList theorem

[Monad m] {f : β → α → m β} {init : β} {xs : Array α} : xs.foldlM f init = xs.toList.foldlM f init

Full source

@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
theorem foldlM_eq_foldlM_toList [Monad m]
    {f : β → α → m β} {init : β} {xs : Array α} :
    xs.foldlM f init = xs.toList.foldlM f init:= by
  simp

Equality of Monadic Left Folds on Array and Its List Representation

Informal description

Let $m$ be a monad, $f : \beta \to \alpha \to m \beta$ a function, and $xs$ an array of elements of type $\alpha$. For any initial value $init : \beta$, the monadic left fold operation applied to $f$ and $init$ over the array $xs$ is equal to the monadic left fold operation applied to $f$ and $init$ over the list representation of $xs$.

Array.foldr_eq_foldr_toList theorem

{f : α → β → β} {init : β} {xs : Array α} : xs.foldr f init = xs.toList.foldr f init

Full source

@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
theorem foldr_eq_foldr_toList {f : α → β → β} {init : β} {xs : Array α} :
    xs.foldr f init = xs.toList.foldr f init := by
  simp

Equality of Right Folds on Array and List Representations

Informal description

For any function $f : \alpha \to \beta \to \beta$, initial value $init : \beta$, and array $xs : \text{Array } \alpha$, the right fold operation on the array $xs$ with function $f$ and initial value $init$ is equal to the right fold operation on the list representation of $xs$ with the same function and initial value. That is, \[ \text{foldr } f \text{ } init \text{ } xs = \text{foldr } f \text{ } init \text{ } (\text{toList } xs). \]

Array.foldl_eq_foldl_toList theorem

{f : β → α → β} {init : β} {xs : Array α} : xs.foldl f init = xs.toList.foldl f init

Full source

@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
theorem foldl_eq_foldl_toList {f : β → α → β} {init : β} {xs : Array α} :
    xs.foldl f init = xs.toList.foldl f init:= by
  simp

Equality of Left Folds on Array and Its List Representation

Informal description

For any binary operation $f : \beta \to \alpha \to \beta$, initial value $init : \beta$, and array $xs$ of elements of type $\alpha$, the left fold of $f$ over the array $xs$ with initial value $init$ is equal to the left fold of $f$ over the list representation of $xs$ with the same initial value.

Array.foldlM_eq_foldlM_data abbrev

Full source

@[deprecated foldlM_toList (since := "2024-09-09")]
abbrev foldlM_eq_foldlM_data := @foldlM_toList

Equality of Monadic Left Folds on Array and List Representations

Informal description

For any monad $m$, function $f : \beta \to \alpha \to m \beta$, initial value $init : \beta$, and array $xs : \text{Array } \alpha$, the monadic left fold operation on the array $xs$ is equal to the monadic left fold operation on the underlying list representation of $xs$. That is, \[ \text{foldlM } f \text{ } init \text{ } xs = \text{foldlM } f \text{ } init \text{ } (\text{toList } xs). \]

Array.foldl_eq_foldl_data abbrev

Full source

@[deprecated foldl_toList (since := "2024-09-09")]
abbrev foldl_eq_foldl_data := @foldl_toList

Equality of Left Folds on Array and Its Data Representation

Informal description

For any binary operation $f : \beta \to \alpha \to \beta$, initial value $init : \beta$, and array $xs : \text{Array } \alpha$, the left fold operation on the array $xs$ is equal to the left fold operation on the underlying data representation of $xs$. That is, \[ \text{foldl } f \text{ } init \text{ } xs = \text{foldl } f \text{ } init \text{ } (\text{data } xs). \]

Array.foldrM_eq_reverse_foldlM_data abbrev

Full source

@[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList

Equivalence of Monadic Right Fold on Arrays and Left Fold on Reversed Lists

Informal description

Let $m$ be a monad, $f : \alpha \to \beta \to m \beta$ a function, $init$ an element of type $\beta$, and $xs$ an array of type $\alpha$. Then the monadic right fold of $xs$ with function $f$ and initial value $init$ is equal to the monadic left fold of the reversed list representation of $xs$ with the flipped function $\lambda x y, f y x$ and initial value $init$.

Array.foldrM_eq_foldrM_data abbrev

Full source

@[deprecated foldrM_toList (since := "2024-09-09")]
abbrev foldrM_eq_foldrM_data := @foldrM_toList

Equivalence of Monadic Right Folds on Array and Its Underlying List Representation

Informal description

Let $m$ be a monad, $f : \alpha \to \beta \to m \beta$ a function, $init$ an element of type $\beta$, and $xs$ an array of type $\alpha$. Then the monadic right fold of $xs$ with function $f$ and initial value $init$ is equal to the monadic right fold of the underlying list representation of $xs$ with the same function and initial value. That is, \[ \text{foldrM } f \text{ } init \text{ } xs = \text{foldrM } f \text{ } init \text{ } (\text{data } xs). \]

Array.foldr_eq_foldr_data abbrev

Full source

@[deprecated foldr_toList (since := "2024-09-09")]
abbrev foldr_eq_foldr_data := @foldr_toList

Equivalence of Right Folds on Array and Its Underlying List Representation

Informal description

For any function $f : \alpha \to \beta \to \beta$, initial value $init : \beta$, and array $xs : \text{Array } \alpha$, the right fold of $xs$ with $f$ and $init$ is equal to the right fold of the underlying list representation of $xs$ with the same function and initial value. That is, \[ \text{foldr } f \text{ } init \text{ } xs = \text{foldr } f \text{ } init \text{ } (\text{data } xs). \]

Array.push_data abbrev

Full source

@[deprecated push_toList (since := "2024-09-09")]
abbrev push_data := @push_toList

Underlying List Representation of Array Push Operation

Informal description

For any array `xs` of type `Array α` and any element `a` of type `α`, the underlying list representation of the array obtained by pushing `a` to `xs` (i.e., `xs.push a`) is equal to the list obtained by appending `[a]` to the list representation of `xs`. In other words, `(xs.push a).data = xs.data ++ [a]`.

Array.toList_eq abbrev

Full source

@[deprecated toListImpl_eq (since := "2024-09-09")]
abbrev toList_eq := @toListImpl_eq

Equivalence of Array-to-List Conversion and Underlying List Representation

Informal description

For any array `xs` of type `Array α`, the list obtained by converting `xs` to a list (`xs.toList`) is equal to the underlying list representation of `xs` (`xs.data`), i.e., `xs.toList = xs.data`.

Array.pop_data abbrev

Full source

@[deprecated pop_toList (since := "2024-09-09")]
abbrev pop_data := @toList_pop

List Representation Preserves Array Pop Operation

Informal description

For any array `xs` of type `Array α`, the list representation of the array after removing its last element (`xs.pop.data`) is equal to the list representation of the original array (`xs.data`) with its last element removed.

Array.append_data abbrev

Full source

@[deprecated toList_append (since := "2024-09-09")]
abbrev append_data := @toList_append

Underlying List Representation Preserves Array Concatenation

Informal description

For any arrays `xs` and `ys` of type `Array α`, the underlying list representation of the concatenated array `xs ++ ys` is equal to the concatenation of the underlying list representations of `xs` and `ys`. That is, $(xs ++ ys).\text{data} = xs.\text{data} ++ ys.\text{data}$.

Array.appendList_data abbrev

Full source

@[deprecated toList_appendList (since := "2024-09-09")]
abbrev appendList_data := @toList_appendList

Underlying List Representation Preserves Array-List Concatenation

Informal description

For any array `xs` of type `Array α` and any list `l` of type `List α`, the underlying list representation of the array obtained by appending `l` to `xs` (`xs.appendList l`) is equal to the concatenation of the underlying list representation of `xs` (`xs.data`) with `l`. In other words, $(xs \mathbin{+\!\!+} l).\text{data} = xs.\text{data} \mathbin{+\!\!+} l$.