Theorems about Array.

Preliminaries about Array needed for List.toArray lemmas.

This section contains only the bare minimum lemmas about Array that we need to write lemmas about List.toArray.

theorem Array.getElem?_eq_getElem {α : Type u_1} {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i]

@[simp]

theorem Array.getElem?_eq_none_iff {α : Type u_1} {i : Nat} {a : Array α} : a[i]? = none ↔ a.size ≤ i

@[simp]

theorem Array.get_eq_getElem {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) : a.get i h = a[i]

@[simp]

theorem Array.get!_eq_getElem! {α : Type u_1} [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]!

@[simp]

theorem Array.mem_toArray {α : Type u_1} {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l

Lemmas about List.toArray.

We prefer to pull List.toArray outwards.

@[simp]

theorem List.size_toArrayAux {α : Type u_1} {a : List α} {b : Array α} : (a.toArrayAux b).size = b.size + a.length

@[simp]

theorem List.push_toArray {α : Type u_1} (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray

@[simp]

theorem List.push_toArray_fun {α : Type u_1} (l : List α) : l.toArray.push = fun (a : α) => (l ++ [a]).toArray

Unapplied variant of push_toArray, useful for monadic reasoning.

@[simp]

theorem List.isEmpty_toArray {α : Type u_1} (l : List α) : l.toArray.isEmpty = l.isEmpty

@[simp]

theorem List.toArray_singleton {α : Type u_1} (a : α) : (List.singleton a).toArray = Array.singleton a

@[simp]

theorem List.back!_toArray {α : Type u_1} [Inhabited α] (l : List α) : l.toArray.back! = l.getLast!

@[simp]

theorem List.back?_toArray {α : Type u_1} (l : List α) : l.toArray.back? = l.getLast?

@[simp]

theorem List.forIn'_loop_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat) (h : i ≤ l.length) (b : β) : Array.forIn'.loop l.toArray f i h b = forIn' (List.drop (l.length - i) l) b fun (a : α) (m : a ∈ List.drop (l.length - i) l) (b : β) => f a ⋯ b

@[simp]

theorem List.forIn'_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) : forIn' l.toArray b f = forIn' l b fun (a : α) (m : a ∈ l) (b : β) => f a ⋯ b

@[simp]

theorem List.forIn_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : forIn l.toArray b f = forIn l b f

theorem List.foldrM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (l : List α) : Array.foldrM f init l.toArray = List.foldrM f init l

theorem List.foldlM_toArray {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (l : List α) : Array.foldlM f init l.toArray = List.foldlM f init l

theorem List.foldr_toArray {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (l : List α) : Array.foldr f init l.toArray = List.foldr f init l

theorem List.foldl_toArray {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (l : List α) : Array.foldl f init l.toArray = List.foldl f init l

@[simp]

theorem List.foldrM_toArray' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : Nat} [Monad m] (f : α → β → m β) (init : β) (l : List α) (h : start = l.toArray.size) : Array.foldrM f init l.toArray start = List.foldrM f init l

Variant of foldrM_toArray with a side condition for the start argument.

@[simp]

theorem List.foldlM_toArray' {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {stop : Nat} [Monad m] (f : β → α → m β) (init : β) (l : List α) (h : stop = l.toArray.size) : Array.foldlM f init l.toArray 0 stop = List.foldlM f init l

Variant of foldlM_toArray with a side condition for the stop argument.

@[simp]

theorem List.foldr_toArray' {α : Type u_1} {β : Type u_2} {start : Nat} (f : α → β → β) (init : β) (l : List α) (h : start = l.toArray.size) : Array.foldr f init l.toArray start = List.foldr f init l

Variant of foldr_toArray with a side condition for the start argument.

@[simp]

theorem List.foldl_toArray' {β : Type u_1} {α : Type u_2} {stop : Nat} (f : β → α → β) (init : β) (l : List α) (h : stop = l.toArray.size) : Array.foldl f init l.toArray 0 stop = List.foldl f init l

Variant of foldl_toArray with a side condition for the stop argument.

@[simp]

theorem List.append_toArray {α : Type u_1} (l₁ l₂ : List α) : l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray

@[simp]

theorem List.push_append_toArray {α : Type u_1} {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a :: bs).toArray

@[simp]

theorem List.foldl_push {α : Type u_1} {l : List α} {as : Array α} : List.foldl Array.push as l = as ++ l.toArray

@[simp]

theorem List.foldr_push {α : Type u_1} {l : List α} {as : Array α} : List.foldr (fun (a : α) (b : Array α) => b.push a) as l = as ++ l.reverse.toArray

@[simp]

theorem List.findSomeM?_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : Array.findSomeM? f l.toArray = List.findSomeM? f l

theorem List.findSomeRevM?_find_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) (i : Nat) (h : i ≤ l.toArray.size) : Array.findSomeRevM?.find f l.toArray i h = List.findSomeM? f (List.take i l).reverse

theorem List.findSomeRevM?_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : Array.findSomeRevM? f l.toArray = List.findSomeM? f l.reverse

theorem List.findRevM?_toArray {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : Array.findRevM? f l.toArray = List.findM? f l.reverse

@[simp]

theorem List.findM?_toArray {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : Array.findM? f l.toArray = List.findM? f l

@[simp]

theorem List.findSome?_toArray {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : Array.findSome? f l.toArray = List.findSome? f l

@[simp]

theorem List.find?_toArray {α : Type} (f : α → Bool) (l : List α) : Array.find? f l.toArray = List.find? f l

@[irreducible]

theorem List.isPrefixOfAux_toArray_succ {α : Type u_1} [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) = l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ i

theorem List.isPrefixOfAux_toArray_succ' {α : Type u_1} [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) = (List.drop (i + 1) l₁).toArray.isPrefixOfAux (List.drop (i + 1) l₂).toArray ⋯ 0

theorem List.isPrefixOfAux_toArray_zero {α : Type u_1} [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) : l₁.toArray.isPrefixOfAux l₂.toArray hle 0 = l₁.isPrefixOf l₂

@[simp]

theorem List.isPrefixOf_toArray {α : Type u_1} [BEq α] (l₁ l₂ : List α) : l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂

@[irreducible]

theorem List.zipWithAux_toArray_succ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) : as.toArray.zipWithAux bs.toArray f (i + 1) cs = as.tail.toArray.zipWithAux bs.tail.toArray f i cs

theorem List.zipWithAux_toArray_succ' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) : as.toArray.zipWithAux bs.toArray f (i + 1) cs = (List.drop (i + 1) as).toArray.zipWithAux (List.drop (i + 1) bs).toArray f 0 cs

theorem List.zipWithAux_toArray_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) : as.toArray.zipWithAux bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray

@[simp]

theorem List.zipWith_toArray {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : α → β → γ) : as.toArray.zipWith bs.toArray f = (List.zipWith f as bs).toArray

@[simp]

theorem List.zip_toArray {α : Type u_1} {β : Type u_2} (as : List α) (bs : List β) : as.toArray.zip bs.toArray = (as.zip bs).toArray

@[irreducible]

theorem List.zipWithAll_go_toArray {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) : Array.zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (List.drop i as) (List.drop i bs)).toArray

@[simp]

theorem List.zipWithAll_toArray {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) (as : List α) (bs : List β) : as.toArray.zipWithAll bs.toArray f = (List.zipWithAll f as bs).toArray

@[simp]

theorem List.toArray_appendList {α : Type u_1} (l₁ l₂ : List α) : l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray

@[simp]

theorem List.pop_toArray {α : Type u_1} (l : List α) : l.toArray.pop = l.dropLast.toArray

@[irreducible]

theorem List.takeWhile_go_succ {α : Type u_1} {r : Array α} (p : α → Bool) (a : α) (l : List α) (i : Nat) : Array.takeWhile.go p (a :: l).toArray (i + 1) r = Array.takeWhile.go p l.toArray i r

theorem List.takeWhile_go_toArray {α : Type u_1} {r : Array α} (p : α → Bool) (l : List α) (i : Nat) : Array.takeWhile.go p l.toArray i r = r ++ (List.takeWhile p (List.drop i l)).toArray

@[simp]

theorem List.takeWhile_toArray {α : Type u_1} (p : α → Bool) (l : List α) : Array.takeWhile p l.toArray = (List.takeWhile p l).toArray

Preliminaries

empty

@[simp]

theorem Array.empty_eq {α : Type u_1} {xs : Array α} : #[] = xs ↔ xs = #[]

size

theorem Array.eq_empty_of_size_eq_zero {α✝ : Type u_1} {l : Array α✝} (h : l.size = 0) : l = #[]

theorem Array.ne_empty_of_size_eq_add_one {n : Nat} {α✝ : Type u_1} {l : Array α✝} (h : l.size = n + 1) : l ≠ #[]

theorem Array.ne_empty_of_size_pos {α✝ : Type u_1} {l : Array α✝} (h : 0 < l.size) : l ≠ #[]

@[simp]

theorem Array.size_eq_zero {α✝ : Type u_1} {l : Array α✝} : l.size = 0 ↔ l = #[]

theorem Array.size_pos_of_mem {α : Type u_1} {a : α} {l : Array α} (h : a ∈ l) : 0 < l.size

theorem Array.exists_mem_of_size_pos {α : Type u_1} {l : Array α} (h : 0 < l.size) : ∃ (a : α), a ∈ l

theorem Array.size_pos_iff_exists_mem {α : Type u_1} {l : Array α} : 0 < l.size ↔ ∃ (a : α), a ∈ l

theorem Array.exists_mem_of_size_eq_add_one {α : Type u_1} {n : Nat} {l : Array α} (h : l.size = n + 1) : ∃ (a : α), a ∈ l

theorem Array.size_pos {α : Type u_1} {l : Array α} : 0 < l.size ↔ l ≠ #[]

theorem Array.size_eq_one {α : Type u_1} {l : Array α} : l.size = 1 ↔ ∃ (a : α), l = #[a]

push

theorem Array.push_ne_empty {α : Type u_1} {a : α} {xs : Array α} : xs.push a ≠ #[]

@[simp]

theorem Array.push_ne_self {α : Type u_1} {a : α} {xs : Array α} : xs.push a ≠ xs

@[simp]

theorem Array.ne_push_self {α : Type u_1} {a : α} {xs : Array α} : xs ≠ xs.push a

theorem Array.back_eq_of_push_eq {α : Type u_1} {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : a = b

theorem Array.pop_eq_of_push_eq {α : Type u_1} {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys

theorem Array.push_inj_left {α : Type u_1} {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs = ys

theorem Array.push_inj_right {α : Type u_1} {a b : α} {xs : Array α} : xs.push a = xs.push b ↔ a = b

theorem Array.push_eq_push {α : Type u_1} {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys

theorem Array.exists_push_of_ne_empty {α : Type u_1} {xs : Array α} (h : xs ≠ #[]) : ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.ne_empty_iff_exists_push {α : Type u_1} {xs : Array α} : xs ≠ #[] ↔ ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.exists_push_of_size_pos {α : Type u_1} {xs : Array α} (h : 0 < xs.size) : ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.size_pos_iff_exists_push {α : Type u_1} {xs : Array α} : 0 < xs.size ↔ ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.exists_push_of_size_eq_add_one {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n + 1) : ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

L[i] and L[i]?

@[deprecated List.getElem_toArray]

theorem Array.getElem_mk {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.length) : { toList := xs }[i] = xs[i]

theorem Array.getElem_eq_getElem_toList {α : Type u_1} {i : Nat} {a : Array α} (h : i < a.size) : a[i] = a.toList[i]

@[simp]

theorem Array.none_eq_getElem?_iff {α : Type u_1} {a : Array α} {i : Nat} : none = a[i]? ↔ a.size ≤ i

theorem Array.getElem?_eq {α : Type u_1} {a : Array α} {i : Nat} : a[i]? = if h : i < a.size then some a[i] else none

theorem Array.getElem?_eq_some_iff {α : Type u_1} {i : Nat} {b : α} {a : Array α} : a[i]? = some b ↔ ∃ (h : i < a.size), a[i] = b

theorem Array.some_eq_getElem?_iff {α : Type u_1} {b : α} {i : Nat} {a : Array α} : some b = a[i]? ↔ ∃ (h : i < a.size), a[i] = b

theorem Array.getElem?_eq_getElem?_toList {α : Type u_1} (a : Array α) (i : Nat) : a[i]? = a.toList[i]?

theorem Array.getElem_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) : let_fun this := ⋯; (a.push x)[i] = a[i]

@[simp]

theorem Array.getElem_push_eq {α : Type u_1} (a : Array α) (x : α) : (a.push x)[a.size] = x

theorem Array.getElem_push {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) : (a.push x)[i] = if h : i < a.size then a[i] else x

@[reducible, inline, deprecated Array.getElem_push]

abbrev Array.get_push {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) : (a.push x)[i] = if h : i < a.size then a[i] else x

Equations

• @Array.get_push = @Array.getElem_push

@[reducible, inline, deprecated Array.getElem_push_lt]

abbrev Array.get_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) : let_fun this := ⋯; (a.push x)[i] = a[i]

Equations

• @Array.get_push_lt = @Array.getElem_push_lt

@[reducible, inline, deprecated Array.getElem_push_eq]

abbrev Array.get_push_eq {α : Type u_1} (a : Array α) (x : α) : (a.push x)[a.size] = x

Equations

• @Array.get_push_eq = @Array.getElem_push_eq

@[simp]

theorem Array.mem_push {α : Type u_1} {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y

theorem Array.mem_push_self {α : Type u_1} {a : Array α} {x : α} : x ∈ a.push x

theorem Array.mem_push_of_mem {α : Type u_1} {a : Array α} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y

theorem Array.getElem_of_mem {α : Type u_1} {a : α} {l : Array α} (h : a ∈ l) : ∃ (n : Nat), ∃ (h : n < l.size), l[n] = a

theorem Array.getElem?_of_mem {α : Type u_1} {a : α} {l : Array α} (h : a ∈ l) : ∃ (n : Nat), l[n]? = some a

theorem Array.mem_of_getElem? {α : Type u_1} {l : Array α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l

theorem Array.mem_iff_getElem {α : Type u_1} {a : α} {l : Array α} : a ∈ l ↔ ∃ (n : Nat), ∃ (h : n < l.size), l[n] = a

theorem Array.mem_iff_getElem? {α : Type u_1} {a : α} {l : Array α} : a ∈ l ↔ ∃ (n : Nat), l[n]? = some a

theorem Array.forall_getElem {α : Type u_1} {l : Array α} {p : α → Prop} : (∀ (n : Nat) (h : n < l.size), p l[n]) ↔ ∀ (a : α), a ∈ l → p a

theorem Array.singleton_inj {α✝ : Type u_1} {a b : α✝} : #[a] = #[b] ↔ a = b

theorem Array.singleton_eq_toArray_singleton {α : Type u_1} (a : α) : #[a] = #[a]

@[simp]

theorem Array.singleton_def {α : Type u_1} (v : α) : Array.singleton v = #[v]

@[simp]

theorem Array.toArray_toList {α : Type u_1} (a : Array α) : a.toList.toArray = a

@[simp]

theorem Array.length_toList {α : Type u_1} {l : Array α} : l.toList.length = l.size

@[simp]

theorem Array.mkEmpty_eq (α : Type u_1) (n : Nat) : Array.mkEmpty n = #[]

@[simp]

theorem Array.size_mk {α : Type u_1} (as : List α) : { toList := as }.size = as.length

@[simp]

theorem Array.isEmpty_toList {α : Type u_1} {l : Array α} : l.toList.isEmpty = l.isEmpty

theorem Array.foldrM_push {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : Array.foldrM f init (arr.push a) = do let init ← f a init Array.foldrM f init arr

@[simp]

theorem Array.foldrM_push' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) {start : Nat} (h : start = arr.size + 1) : Array.foldrM f init (arr.push a) start = do let init ← f a init Array.foldrM f init arr

Variant of foldrM_push with h : start = arr.size + 1 rather than (arr.push a).size as the argument.

theorem Array.foldr_push {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α) (a : α) : Array.foldr f init (arr.push a) = Array.foldr f (f a init) arr

@[simp]

theorem Array.foldr_push' {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α) (a : α) {start : Nat} (h : start = arr.size + 1) : Array.foldr f init (arr.push a) start = Array.foldr f (f a init) arr

Variant of foldr_push with the h : start = arr.size + 1 rather than (arr.push a).size as the argument.

@[inline]

def Array.toListRev {α : Type u_1} (arr : Array α) : List α

A more efficient version of arr.toList.reverse.

Equations

• arr.toListRev = Array.foldl (fun (l : List α) (t : α) => t :: l) [] arr

@[simp]

theorem Array.toListRev_eq {α : Type u_1} (arr : Array α) : arr.toListRev = arr.toList.reverse

theorem Array.mapM_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : Array.mapM f arr = Array.foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) #[] arr

@[irreducible]

theorem Array.mapM_eq_foldlM.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) (i : Nat) (r : Array β) : Array.mapM.map f arr i r = List.foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) r (List.drop i arr.toList)

@[simp]

theorem Array.toList_map {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : (Array.map f arr).toList = List.map f arr.toList

@[simp]

theorem Array.size_map {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : (Array.map f arr).size = arr.size

@[simp]

theorem Array.mapM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : Array.mapM f #[] = pure #[]

@[simp]

theorem Array.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) : Array.map f #[] = #[]

@[simp]

theorem Array.appendList_nil {α : Type u_1} (arr : Array α) : arr ++ [] = arr

@[simp]

theorem Array.appendList_cons {α : Type u_1} (arr : Array α) (a : α) (l : List α) : arr ++ a :: l = arr.push a ++ l

@[simp]

theorem Array.toList_appendList {α : Type u_1} (arr : Array α) (l : List α) : (arr ++ l).toList = arr.toList ++ l

theorem Array.foldl_toList_eq_flatMap {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β) (H : ∀ (acc : Array β) (a : α), (F acc a).toList = acc.toList ++ G a) : (List.foldl F acc l).toList = acc.toList ++ l.flatMap G

theorem Array.foldl_toList_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (G : α → β) : (List.foldl (fun (acc : Array β) (a : α) => acc.push (G a)) acc l).toList = acc.toList ++ List.map G l

theorem Array.anyM_eq_anyM_loop {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) (start stop : Nat) : Array.anyM p as start stop = Array.anyM.loop p as (min stop as.size) ⋯ start

theorem Array.anyM_stop_le_start {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) (start stop : Nat) (h : min stop as.size ≤ start) : Array.anyM p as start stop = pure false

@[simp]

theorem Array.not_mem_empty {α : Type u_1} (a : α) : ¬a ∈ #[]

uset

theorem Array.size_uset {α : Type u_1} (a : Array α) (v : α) (i : USize) (h : i.toNat < a.size) : (a.uset i v h).size = a.size

get

theorem Array.getElem?_lt {α : Type u_1} (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i]

theorem Array.getElem?_ge {α : Type u_1} (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none

@[simp]

theorem Array.get?_eq_getElem? {α : Type u_1} (a : Array α) (i : Nat) : a.get? i = a[i]?

theorem Array.getElem?_len_le {α : Type u_1} (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none

theorem Array.getD_get? {α : Type u_1} (a : Array α) (i : Nat) (d : α) : a[i]?.getD d = if p : i < a.size then a[i] else d

@[simp]

theorem Array.getD_eq_get? {α : Type u_1} (a : Array α) (n : Nat) (d : α) : a.getD n d = a[n]?.getD d

theorem Array.get!_eq_getD {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) : a.get! n = a.getD n default

@[simp]

theorem Array.get!_eq_getElem? {α : Type u_1} [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default

set

@[simp]

theorem Array.getElem_set_eq {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat} (eq : i = j) (p : j < (a.set i v h).size) : (a.set i v h)[j] = v

@[simp]

theorem Array.getElem_set_ne {α : Type u_1} (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat} (pj : j < (a.set i v h').size) (h : i ≠ j) : (a.set i v h')[j] = a[j]

theorem Array.getElem_set {α : Type u_1} (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat) (h : j < (a.set i v h').size) : (a.set i v h')[j] = if i = j then v else a[j]

@[simp]

theorem Array.getElem?_set_eq {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) (v : α) : (a.set i v h)[i]? = some v

@[simp]

theorem Array.getElem?_set_ne {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α) (ne : i ≠ j) : (a.set i v h)[j]? = a[j]?

setIfInBounds

@[simp]

theorem Array.set!_is_setIfInBounds : @Array.set! = @Array.setIfInBounds

@[simp]

theorem Array.size_setIfInBounds {α : Type u_1} (a : Array α) (index : Nat) (val : α) : (a.setIfInBounds index val).size = a.size

@[simp]

theorem Array.getElem_setIfInBounds_eq {α : Type u_1} (a : Array α) {i : Nat} (v : α) (h : i < (a.setIfInBounds i v).size) : (a.setIfInBounds i v)[i] = v

@[simp]

theorem Array.getElem?_setIfInBounds_eq {α : Type u_1} (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setIfInBounds i v)[i]? = some v

@[simp]

theorem Array.getD_get?_setIfInBounds {α : Type u_1} (a : Array α) (i : Nat) (v d : α) : (a.setIfInBounds i v)[i]?.getD d = if i < a.size then v else d

Simplifies a normal form from get!

ofFn

@[simp, irreducible]

theorem Array.size_ofFn_go {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) (acc : Array α) : (Array.ofFn.go f i acc).size = acc.size + (n - i)

@[simp]

theorem Array.size_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (Array.ofFn f).size = n

@[irreducible]

theorem Array.getElem_ofFn_go {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) {acc : Array α} {k : Nat} (hki : k < n) (hin : i ≤ n) (hi : i = acc.size) (hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩) : (Array.ofFn.go f i acc)[k] = f ⟨k, hki⟩

@[simp]

theorem Array.getElem_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) (h : i < (Array.ofFn f).size) : (Array.ofFn f)[i] = f ⟨i, ⋯⟩

theorem Array.getElem?_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) : (Array.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

@[simp]

theorem Array.ofFn_zero {α : Type u_1} (f : Fin 0 → α) : Array.ofFn f = #[]

theorem Array.ofFn_succ {n : Nat} {α : Type u_1} (f : Fin (n + 1) → α) : Array.ofFn f = (Array.ofFn fun (i : Fin n) => f i.castSucc).push (f ⟨n, ⋯⟩)

mkArray

@[simp]

theorem Array.size_mkArray {α : Type u_1} (n : Nat) (v : α) : (mkArray n v).size = n

@[simp]

theorem Array.toList_mkArray {α : Type u_1} (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v

theorem Array.mkArray_eq_toArray_replicate {α : Type u_1} (n : Nat) (v : α) : mkArray n v = (List.replicate n v).toArray

@[simp]

theorem Array.getElem_mkArray {α : Type u_1} {i : Nat} (n : Nat) (v : α) (h : i < (mkArray n v).size) : (mkArray n v)[i] = v

theorem Array.getElem?_mkArray {α : Type u_1} (n : Nat) (v : α) (i : Nat) : (mkArray n v)[i]? = if i < n then some v else none

mem

@[simp]

theorem Array.mem_toList {α : Type u_1} {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l

theorem Array.not_mem_nil {α : Type u_1} (a : α) : ¬a ∈ #[]

@[simp]

theorem Array.mem_dite_empty_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : ¬p → Array α} : (x ∈ if h : p then #[] else l h) ↔ ∃ (h : ¬p), x ∈ l h

@[simp]

theorem Array.mem_dite_empty_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : p → Array α} : (x ∈ if h : p then l h else #[]) ↔ ∃ (h : p), x ∈ l h

@[simp]

theorem Array.mem_ite_empty_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Array α} : (x ∈ if p then #[] else l) ↔ ¬p ∧ x ∈ l

@[simp]

theorem Array.mem_ite_empty_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Array α} : (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l

get lemmas

theorem Array.lt_of_getElem {α : Type u_1} {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} : a[idx] = x → idx < a.size

theorem Array.getElem_fin_eq_getElem_toList {α : Type u_1} (a : Array α) (i : Fin a.size) : a[i] = a.toList[i]

@[simp]

theorem Array.ugetElem_eq_getElem {α : Type u_1} (a : Array α) {i : USize} (h : i.toNat < a.size) : a[i] = a[i.toNat]

theorem Array.getElem?_size_le {α : Type u_1} (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none

@[reducible, inline, deprecated Array.getElem?_size_le]

abbrev Array.get?_len_le {α : Type u_1} (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none

Equations

• @Array.get?_len_le = @Array.getElem?_size_le

theorem Array.getElem_mem_toList {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) : a[i] ∈ a.toList

theorem Array.get?_eq_get?_toList {α : Type u_1} (a : Array α) (i : Nat) : a.get? i = a.toList.get? i

theorem Array.get!_eq_get? {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default

theorem Array.back!_eq_back? {α : Type u_1} [Inhabited α] (a : Array α) : a.back! = a.back?.getD default

@[simp]

theorem Array.back?_push {α : Type u_1} {x : α} (a : Array α) : (a.push x).back? = some x

@[simp]

theorem Array.back!_push {α : Type u_1} {x : α} [Inhabited α] (a : Array α) : (a.push x).back! = x

theorem Array.mem_of_back?_eq_some {α : Type u_1} {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs

theorem Array.getElem?_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) : (a.push x)[i]? = some a[i]

@[reducible, inline, deprecated Array.getElem?_push_lt]

abbrev Array.get?_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) : (a.push x)[i]? = some a[i]

Equations

• @Array.get?_push_lt = @Array.getElem?_push_lt

theorem Array.getElem?_push_eq {α : Type u_1} (a : Array α) (x : α) : (a.push x)[a.size]? = some x

@[reducible, inline, deprecated Array.getElem?_push_eq]

abbrev Array.get?_push_eq {α : Type u_1} (a : Array α) (x : α) : (a.push x)[a.size]? = some x

Equations

• @Array.get?_push_eq = @Array.getElem?_push_eq

theorem Array.getElem?_push {α : Type u_1} {x : α} {i : Nat} {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]?

@[reducible, inline, deprecated Array.getElem?_push]

abbrev Array.get?_push {α : Type u_1} {x : α} {i : Nat} {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]?

Equations

• @Array.get?_push = @Array.getElem?_push

@[simp]

theorem Array.getElem?_size {α : Type u_1} {a : Array α} : a[a.size]? = none

@[reducible, inline, deprecated Array.getElem?_size]

abbrev Array.get?_size {α : Type u_1} {a : Array α} : a[a.size]? = none

Equations

• @Array.get?_size = @Array.getElem?_size

@[simp]

theorem Array.toList_set {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size) : (a.set i v h).toList = a.toList.set i v

theorem Array.get_set_eq {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size) : (a.set i v h)[i] = v

theorem Array.get?_set_eq {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size) : (a.set i v h)[i]? = some v

@[simp]

theorem Array.get?_set_ne {α : Type u_1} (a : Array α) (i : Nat) (h' : i < a.size) {j : Nat} (v : α) (h : i ≠ j) : (a.set i v h')[j]? = a[j]?

theorem Array.get?_set {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) (j : Nat) (v : α) : (a.set i v h)[j]? = if i = j then some v else a[j]?

theorem Array.get_set {α : Type u_1} (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) : (a.set i v hi)[j] = if i = j then v else a[j]

@[simp]

theorem Array.get_set_ne {α : Type u_1} (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size) (h : i ≠ j) : (a.set i v hi)[j] = a[j]

theorem Array.getElem_setIfInBounds {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < (a.setIfInBounds i v).size) : (a.setIfInBounds i v)[i] = v

theorem Array.set_set {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) (v v' : α) : (a.set i v h).set i v' ⋯ = a.set i v' h

theorem Array.swap_def {α : Type u_1} (a : Array α) (i j : Nat) (hi : i < a.size) (hj : j < a.size) : a.swap i j hi hj = (a.set i a[j] hi).set j a[i] ⋯

@[simp]

theorem Array.toList_swap {α : Type u_1} (a : Array α) (i j : Nat) (hi : i < a.size) (hj : j < a.size) : (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i]

theorem Array.getElem?_swap {α : Type u_1} (a : Array α) (i j : Nat) (hi : i < a.size) (hj : j < a.size) (k : Nat) : (a.swap i j hi hj)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[k]?

@[simp]

theorem Array.swapAt_def {α : Type u_1} (a : Array α) (i : Nat) (v : α) (hi : i < a.size) : a.swapAt i v hi = (a[i], a.set i v hi)

@[simp]

theorem Array.size_swapAt {α : Type u_1} (a : Array α) (i : Nat) (v : α) (hi : i < a.size) : (a.swapAt i v hi).snd.size = a.size

@[simp]

theorem Array.swapAt!_def {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size) : a.swapAt! i v = (a[i], a.set i v h)

@[simp]

theorem Array.size_swapAt! {α : Type u_1} (a : Array α) (i : Nat) (v : α) : (a.swapAt! i v).snd.size = a.size

@[simp]

theorem Array.toList_pop {α : Type u_1} (a : Array α) : a.pop.toList = a.toList.dropLast

@[simp]

theorem Array.pop_empty {α : Type u_1} : #[].pop = #[]

@[simp]

theorem Array.pop_push {α : Type u_1} {x : α} (a : Array α) : (a.push x).pop = a

@[simp]

theorem Array.getElem_pop {α : Type u_1} (a : Array α) (i : Nat) (hi : i < a.pop.size) : a.pop[i] = a[i]

theorem Array.eq_push_pop_back!_of_size_ne_zero {α : Type u_1} [Inhabited α] {as : Array α} (h : as.size ≠ 0) : as = as.pop.push as.back!

theorem Array.eq_push_of_size_ne_zero {α : Type u_1} {as : Array α} (h : as.size ≠ 0) : ∃ (bs : Array α), ∃ (c : α), as = bs.push c

theorem Array.size_eq_length_toList {α : Type u_1} (as : Array α) : as.size = as.toList.length

@[simp]

theorem Array.size_swapIfInBounds {α : Type u_1} (a : Array α) (i j : Nat) : (a.swapIfInBounds i j).size = a.size

@[reducible, inline, deprecated Array.size_swapIfInBounds]

abbrev Array.size_swap! {α : Type u_1} (a : Array α) (i j : Nat) : (a.swapIfInBounds i j).size = a.size

Equations

• @Array.size_swap! = @Array.size_swapIfInBounds

@[simp]

theorem Array.size_reverse {α : Type u_1} (a : Array α) : a.reverse.size = a.size

@[irreducible]

theorem Array.size_reverse.go {α : Type u_1} (as : Array α) (i : Nat) (j : Fin as.size) : (Array.reverse.loop as i j).size = as.size

@[simp]

theorem Array.size_range {n : Nat} : (Array.range n).size = n

@[simp]

theorem Array.toList_range (n : Nat) : (Array.range n).toList = List.range n

@[simp]

theorem Array.getElem_range {n x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x

@[simp]

theorem Array.toList_reverse {α : Type u_1} (a : Array α) : a.reverse.toList = a.toList.reverse

@[irreducible]

theorem Array.toList_reverse.go {α : Type u_1} (a as : Array α) (i j : Nat) (hj : j < as.size) (h : i + j + 1 = a.size) (h₂ : as.size = a.size) (H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?) (k : Nat) : (Array.reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]?

BEq

@[simp]

theorem Array.reflBEq_iff {α : Type u_1} [BEq α] : ReflBEq (Array α) ↔ ReflBEq α

@[simp]

theorem Array.lawfulBEq_iff {α : Type u_1} [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α

take

@[simp]

theorem Array.size_take_loop {α : Type u_1} (a : Array α) (n : Nat) : (Array.take.loop n a).size = a.size - n

@[simp]

theorem Array.getElem_take_loop {α : Type u_1} (a : Array α) (n i : Nat) (h : i < (Array.take.loop n a).size) : (Array.take.loop n a)[i] = a[i]

@[simp]

theorem Array.size_take {α : Type u_1} (a : Array α) (n : Nat) : (a.take n).size = min n a.size

@[simp]

theorem Array.getElem_take {α : Type u_1} (a : Array α) (n i : Nat) (h : i < (a.take n).size) : (a.take n)[i] = a[i]

@[simp]

theorem Array.toList_take {α : Type u_1} (a : Array α) (n : Nat) : (a.take n).toList = List.take n a.toList

forIn

@[simp]

theorem Array.forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : forIn as.toList b f = forIn as b f

@[simp]

theorem Array.forIn'_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as.toList → β → m (ForInStep β)) : forIn' as.toList b f = forIn' as b fun (a : α) (m : a ∈ as) (b : β) => f a ⋯ b

foldl / foldr

@[simp]

theorem Array.foldlM_loop_empty {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {s : Nat} {h : s ≤ #[].size} [Monad m] (f : β → α → m β) (init : β) (i j : Nat) : Array.foldlM.loop f #[] s h i j init = pure init

@[simp]

theorem Array.foldlM_empty {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {start stop : Nat} [Monad m] (f : β → α → m β) (init : β) : Array.foldlM f init #[] start stop = pure init

@[simp]

theorem Array.foldrM_fold_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (i j : Nat) (h : j ≤ #[].size) : Array.foldrM.fold f #[] i j h init = pure init

@[simp]

theorem Array.foldrM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start stop : Nat} [Monad m] (f : α → β → m β) (init : β) : Array.foldrM f init #[] start stop = pure init

theorem Array.foldl_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])) : motive as.size (Array.foldl f init as)

@[irreducible]

theorem Array.foldl_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {f : β → α → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])) {i j : Nat} {b : β} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) : motive as.size (Array.foldlM.loop f as as.size ⋯ i j b)

theorem Array.foldr_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)) : motive 0 (Array.foldr f init as)

@[irreducible]

theorem Array.foldr_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {f : α → β → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)) {i : Nat} {b : β} (hi : i ≤ as.size) (H : motive i b) : motive 0 (Array.foldrM.fold f as 0 i hi b)

theorem Array.foldl_congr {α : Type u_1} {β : Type u_2} {as bs : Array α} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g) {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') : Array.foldl f a as start stop = Array.foldl g b bs start' stop'

theorem Array.foldr_congr {α : Type u_1} {β : Type u_2} {as bs : Array α} (h₀ : as = bs) {f g : α → β → β} (h₁ : f = g) {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') : Array.foldr f a as start stop = Array.foldr g b bs start' stop'

theorem Array.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} (f : β → α → β) (b : β) (l : Array α) : Array.foldl f b l = Array.foldlM f b l

theorem Array.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : Array α) : Array.foldr f b l = Array.foldrM f b l

@[simp]

theorem Array.id_run_foldlM {β : Type u_1} {α : Type u_2} (f : β → α → Id β) (b : β) (l : Array α) : (Array.foldlM f b l).run = Array.foldl f b l

@[simp]

theorem Array.id_run_foldrM {α : Type u_1} {β : Type u_2} (f : α → β → Id β) (b : β) (l : Array α) : (Array.foldrM f b l).run = Array.foldr f b l

theorem Array.foldl_hom {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : Array β) (init : α₁) (H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) : Array.foldl g₂ (f init) l = f (Array.foldl g₁ init l)

theorem Array.foldr_hom {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : Array α) (init : β₁) (H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) : Array.foldr g₂ (f init) l = f (Array.foldr g₁ init l)

map

@[simp]

theorem Array.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : Array α} : b ∈ Array.map f l ↔ ∃ (a : α), a ∈ l ∧ f a = b

theorem Array.exists_of_mem_map {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : Array α✝} {b : α✝¹} (h : b ∈ Array.map f l) : ∃ (a : α✝), a ∈ l ∧ f a = b

theorem Array.mem_map_of_mem {α : Type u_1} {β : Type u_2} {l : Array α} {a : α} (f : α → β) (h : a ∈ l) : f a ∈ Array.map f l

theorem Array.mapM_eq_mapM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : Array.mapM f arr = List.toArray <$> List.mapM f arr.toList

@[simp]

theorem Array.toList_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : Array.toList <$> Array.mapM f arr = List.mapM f arr.toList

@[irreducible]

theorem Array.mapM_map_eq_foldl {α : Type u_1} {β : Type u_2} {b : Array β} (as : Array α) (f : α → β) (i : Nat) : Array.mapM.map f as i b = Array.foldl (fun (r : Array β) (a : α) => r.push (f a)) b as i

theorem Array.map_eq_foldl {α : Type u_1} {β : Type u_2} (as : Array α) (f : α → β) : Array.map f as = Array.foldl (fun (r : Array β) (a : α) => r.push (f a)) #[] as

theorem Array.map_induction {α : Type u_1} {β : Type u_2} (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0) (p : Fin as.size → β → Prop) (hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)) : motive as.size ∧ ∃ (eq : (Array.map f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (Array.map f as)[i]

theorem Array.map_spec {α : Type u_1} {β : Type u_2} (as : Array α) (f : α → β) (p : Fin as.size → β → Prop) (hs : ∀ (i : Fin as.size), p i (f as[i])) : ∃ (eq : (Array.map f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (Array.map f as)[i]

@[simp]

theorem Array.getElem_map {α : Type u_1} {β : Type u_2} (f : α → β) (as : Array α) (i : Nat) (h : i < (Array.map f as).size) : (Array.map f as)[i] = f as[i]

@[simp]

theorem Array.getElem?_map {α : Type u_1} {β : Type u_2} (f : α → β) (as : Array α) (i : Nat) : (Array.map f as)[i]? = Option.map f as[i]?

@[simp]

theorem Array.map_push {α : Type u_1} {β : Type u_2} {f : α → β} {as : Array α} {x : α} : Array.map f (as.push x) = (Array.map f as).push (f x)

@[simp]

theorem Array.map_pop {α : Type u_1} {β : Type u_2} {f : α → β} {as : Array α} : Array.map f as.pop = (Array.map f as).pop

modify

@[simp]

theorem Array.size_modify {α : Type u_1} (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size

theorem Array.getElem_modify {α : Type u_1} {f : α → α} {as : Array α} {x i : Nat} (h : i < (as.modify x f).size) : (as.modify x f)[i] = if x = i then f as[i] else as[i]

@[simp]

theorem Array.toList_modify {α : Type u_1} {x : Nat} (as : Array α) (f : α → α) : (as.modify x f).toList = List.modify f x as.toList

theorem Array.getElem_modify_self {α : Type u_1} {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) : (as.modify i f)[i] = f as[i]

theorem Array.getElem_modify_of_ne {α : Type u_1} {j : Nat} {as : Array α} {i : Nat} (h : i ≠ j) (f : α → α) (hj : j < (as.modify i f).size) : (as.modify i f)[j] = as[j]

theorem Array.getElem?_modify {α : Type u_1} {as : Array α} {i : Nat} {f : α → α} {j : Nat} : (as.modify i f)[j]? = if i = j then Option.map f as[j]? else as[j]?

filter

@[simp]

theorem Array.toList_filter {α : Type u_1} (p : α → Bool) (l : Array α) : (Array.filter p l).toList = List.filter p l.toList

@[simp]

theorem Array.filter_filter {α : Type u_1} {p : α → Bool} (q : α → Bool) (l : Array α) : Array.filter p (Array.filter q l) = Array.filter (fun (a : α) => p a && q a) l

@[simp]

theorem Array.mem_filter {α✝ : Type u_1} {p : α✝ → Bool} {as : Array α✝} {x : α✝} : x ∈ Array.filter p as ↔ x ∈ as ∧ p x = true

theorem Array.mem_of_mem_filter {α : Type u_1} {p : α → Bool} {a : α} {l : Array α} (h : a ∈ Array.filter p l) : a ∈ l

theorem Array.filter_congr {α : Type u_1} {as bs : Array α} (h : as = bs) {f g : α → Bool} (h' : f = g) {start stop start' stop' : Nat} (h₁ : start = start') (h₂ : stop = stop') : Array.filter f as start stop = Array.filter g bs start' stop'

filterMap

@[simp]

theorem Array.toList_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : Array α) : (Array.filterMap f l).toList = List.filterMap f l.toList

@[simp]

theorem Array.mem_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : Array α} {b : β} : b ∈ Array.filterMap f l ↔ ∃ (a : α), a ∈ l ∧ f a = some b

theorem Array.filterMap_congr {α : Type u_1} {β : Type u_2} {as bs : Array α} (h : as = bs) {f g : α → Option β} (h' : f = g) {start stop start' stop' : Nat} (h₁ : start = start') (h₂ : stop = stop') : Array.filterMap f as start stop = Array.filterMap g bs start' stop'

empty

theorem Array.size_empty {α : Type u_1} : #[].size = 0

append

theorem Array.push_eq_append_singleton {α : Type u_1} (as : Array α) (x : α) : as.push x = as ++ #[x]

@[simp]

theorem Array.mem_append {α : Type u_1} {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

theorem Array.mem_append_left {α : Type u_1} {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂

theorem Array.mem_append_right {α : Type u_1} {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂

@[simp]

theorem Array.size_append {α : Type u_1} (as bs : Array α) : (as ++ bs).size = as.size + bs.size

@[simp]

theorem Array.empty_append {α : Type u_1} (as : Array α) : #[] ++ as = as

@[simp]

theorem Array.append_empty {α : Type u_1} (as : Array α) : as ++ #[] = as

theorem Array.getElem_append {α : Type u_1} {i : Nat} {as bs : Array α} (h : i < (as ++ bs).size) : (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]

theorem Array.getElem_append_left {α : Type u_1} {i : Nat} {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) : (as ++ bs)[i] = as[i]

theorem Array.getElem_append_right {α : Type u_1} {i : Nat} {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) (hlt : i - as.size < bs.size := ⋯) : (as ++ bs)[i] = bs[i - as.size]

theorem Array.getElem?_append_left {α : Type u_1} {as bs : Array α} {n : Nat} (hn : n < as.size) : (as ++ bs)[n]? = as[n]?

theorem Array.getElem?_append_right {α : Type u_1} {as bs : Array α} {n : Nat} (h : as.size ≤ n) : (as ++ bs)[n]? = bs[n - as.size]?

theorem Array.getElem?_append {α : Type u_1} {as bs : Array α} {n : Nat} : (as ++ bs)[n]? = if n < as.size then as[n]? else bs[n - as.size]?

@[simp]

theorem Array.toArray_eq_append_iff {α : Type u_1} {xs : List α} {as bs : Array α} : xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList

@[simp]

theorem Array.append_eq_toArray_iff {α : Type u_1} {as bs : Array α} {xs : List α} : as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs

flatten

@[simp]

theorem Array.toList_flatten {α : Type u_1} {l : Array (Array α)} : l.flatten.toList = (List.map Array.toList l.toList).flatten

theorem Array.mem_flatten {α : Type u_1} {a : α} {L : Array (Array α)} : a ∈ L.flatten ↔ ∃ (l : Array α), l ∈ L ∧ a ∈ l

extract

theorem Array.extract_loop_zero {α : Type u_1} (as bs : Array α) (start : Nat) : Array.extract.loop as 0 start bs = bs

theorem Array.extract_loop_succ {α : Type u_1} (as bs : Array α) (size start : Nat) (h : start < as.size) : Array.extract.loop as (size + 1) start bs = Array.extract.loop as size (start + 1) (bs.push as[start])

theorem Array.extract_loop_of_ge {α : Type u_1} (as bs : Array α) (size start : Nat) (h : start ≥ as.size) : Array.extract.loop as size start bs = bs

theorem Array.extract_loop_eq_aux {α : Type u_1} (as bs : Array α) (size start : Nat) : Array.extract.loop as size start bs = bs ++ Array.extract.loop as size start #[]

theorem Array.extract_loop_eq {α : Type u_1} (as bs : Array α) (size start : Nat) (h : start + size ≤ as.size) : Array.extract.loop as size start bs = bs ++ as.extract start (start + size)

theorem Array.size_extract_loop {α : Type u_1} (as bs : Array α) (size start : Nat) : (Array.extract.loop as size start bs).size = bs.size + min size (as.size - start)

@[simp]

theorem Array.size_extract {α : Type u_1} (as : Array α) (start stop : Nat) : (as.extract start stop).size = min stop as.size - start

theorem Array.getElem_extract_loop_lt_aux {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hlt : i < bs.size) : i < (Array.extract.loop as size start bs).size

theorem Array.getElem_extract_loop_lt {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hlt : i < bs.size) (h : i < (Array.extract.loop as size start bs).size := ⋯) : (Array.extract.loop as size start bs)[i] = bs[i]

theorem Array.getElem_extract_loop_ge_aux {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size) (h : i < (Array.extract.loop as size start bs).size) : start + i - bs.size < as.size

theorem Array.getElem_extract_loop_ge {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size) (h : i < (Array.extract.loop as size start bs).size) (h' : start + i - bs.size < as.size := ⋯) : (Array.extract.loop as size start bs)[i] = as[start + i - bs.size]

theorem Array.getElem_extract_aux {α : Type u_1} {i : Nat} {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) : start + i < as.size

@[simp]

theorem Array.getElem_extract {α : Type u_1} {i : Nat} {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) : (as.extract start stop)[i] = as[start + i]

theorem Array.getElem?_extract {α : Type u_1} {i : Nat} {as : Array α} {start stop : Nat} : (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none

@[simp]

theorem Array.toList_extract {α : Type u_1} (as : Array α) (start stop : Nat) : (as.extract start stop).toList = List.take (stop - start) (List.drop start as.toList)

@[simp]

theorem Array.extract_all {α : Type u_1} (as : Array α) : as.extract 0 as.size = as

theorem Array.extract_empty_of_stop_le_start {α : Type u_1} (as : Array α) {start stop : Nat} (h : stop ≤ start) : as.extract start stop = #[]

theorem Array.extract_empty_of_size_le_start {α : Type u_1} (as : Array α) {start stop : Nat} (h : as.size ≤ start) : as.extract start stop = #[]

@[simp]

theorem Array.extract_empty {α : Type u_1} (start stop : Nat) : #[].extract start stop = #[]

any

@[irreducible]

theorem Array.anyM_loop_cons {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) : Array.anyM.loop p { toList := a :: as } (stop + 1) h (start + 1) = Array.anyM.loop p { toList := as } stop ⋯ start

@[simp, irreducible]

theorem Array.anyM_toList {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) : List.anyM p as.toList = Array.anyM p as

@[irreducible]

theorem Array.anyM_loop_iff_exists {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : Nat} (h : stop ≤ as.size) : Array.anyM.loop p as stop h start = true ↔ ∃ (i : Fin as.size), start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true

theorem Array.any_iff_exists {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : Nat} : as.any p start stop = true ↔ ∃ (i : Fin as.size), start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true

theorem Array.any_eq_true {α : Type u_1} {p : α → Bool} {as : Array α} : as.any p = true ↔ ∃ (i : Fin as.size), p as[i] = true

theorem Array.any_toList {α : Type u_1} {p : α → Bool} (as : Array α) : as.toList.any p = as.any p

all

theorem Array.allM_eq_not_anyM_not {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) : Array.allM p as = (fun (x : Bool) => !x) <$> Array.anyM (fun (x : α) => (fun (x : Bool) => !x) <$> p x) as

@[simp]

theorem Array.allM_toList {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) : List.allM p as.toList = Array.allM p as

theorem Array.all_eq_not_any_not {α : Type u_1} (p : α → Bool) (as : Array α) (start stop : Nat) : as.all p start stop = !as.any (fun (x : α) => !p x) start stop

theorem Array.all_iff_forall {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : Nat} : as.all p start stop = true ↔ ∀ (i : Fin as.size), start ≤ ↑i ∧ ↑i < stop → p as[i] = true

theorem Array.all_eq_true {α : Type u_1} {p : α → Bool} {as : Array α} : as.all p = true ↔ ∀ (i : Fin as.size), p as[i] = true

theorem Array.all_toList {α : Type u_1} {p : α → Bool} (as : Array α) : as.toList.all p = as.all p

theorem Array.all_eq_true_iff_forall_mem {α : Type u_1} {p : α → Bool} {l : Array α} : l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

contains

theorem Array.contains_def {α : Type u_1} [DecidableEq α] {a : α} {as : Array α} : as.contains a = true ↔ a ∈ as

instance Array.instDecidableMemOfDecidableEq {α : Type u_1} [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as)

swap

@[simp]

theorem Array.getElem_swap_right {α : Type u_1} (a : Array α) {i j : Nat} {hi : i < a.size} {hj : j < a.size} : (a.swap i j hi hj)[j] = a[i]

@[simp]

theorem Array.getElem_swap_left {α : Type u_1} (a : Array α) {i j : Nat} {hi : i < a.size} {hj : j < a.size} : (a.swap i j hi hj)[i] = a[j]

@[simp]

theorem Array.getElem_swap_of_ne {α : Type u_1} {p : Nat} (a : Array α) {i j : Nat} {hi : i < a.size} {hj : j < a.size} (hp : p < a.size) (hi' : p ≠ i) (hj' : p ≠ j) : (a.swap i j hi hj)[p] = a[p]

theorem Array.getElem_swap' {α : Type u_1} (a : Array α) (i j : Nat) {hi : i < a.size} {hj : j < a.size} (k : Nat) (hk : k < a.size) : (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

theorem Array.getElem_swap {α : Type u_1} (a : Array α) (i j : Nat) {hi : i < a.size} {hj : j < a.size} (k : Nat) (hk : k < (a.swap i j hi hj).size) : (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

@[simp]

theorem Array.swap_swap {α : Type u_1} (a : Array α) {i j : Nat} (hi : i < a.size) (hj : j < a.size) : (a.swap i j hi hj).swap i j ⋯ ⋯ = a

theorem Array.swap_comm {α : Type u_1} (a : Array α) {i j : Nat} {hi : i < a.size} {hj : j < a.size} : a.swap i j hi hj = a.swap j i hj hi

eraseIdx

theorem Array.eraseIdx_eq_eraseIdxIfInBounds {α : Type u_1} {a : Array α} {i : Nat} (h : i < a.size) : a.eraseIdx i h = a.eraseIdxIfInBounds i

isPrefixOf

@[simp]

theorem Array.isPrefixOf_toList {α : Type u_1} [BEq α] {as bs : Array α} : as.toList.isPrefixOf bs.toList = as.isPrefixOf bs

zipWith

@[simp]

theorem Array.toList_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) : (as.zipWith bs f).toList = List.zipWith f as.toList bs.toList

@[simp]

theorem Array.toList_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) : (as.zip bs).toList = as.toList.zip bs.toList

@[simp]

theorem Array.toList_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) : (as.zipWithAll bs f).toList = List.zipWithAll f as.toList bs.toList

@[simp]

theorem Array.size_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : α → β → γ) : (as.zipWith bs f).size = min as.size bs.size

@[simp]

theorem Array.size_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) : (as.zip bs).size = min as.size bs.size

findSomeM?, findM?, findSome?, find?

@[simp]

theorem Array.findSomeM?_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (p : α → m (Option β)) (as : Array α) : List.findSomeM? p as.toList = Array.findSomeM? p as

@[simp]

theorem Array.findM?_toList {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) : List.findM? p as.toList = Array.findM? p as

@[simp]

theorem Array.findSome?_toList {α : Type u_1} {β : Type u_2} (p : α → Option β) (as : Array α) : List.findSome? p as.toList = Array.findSome? p as

@[simp]

theorem Array.find?_toList {α : Type} (p : α → Bool) (as : Array α) : List.find? p as.toList = Array.find? p as

More theorems about List.toArray, followed by an Array operation.

Our goal is to have simp "pull List.toArray outwards" as much as possible.

@[simp]

theorem List.toListRev_toArray {α : Type u_1} (l : List α) : l.toArray.toListRev = l.reverse

@[simp]

theorem List.take_toArray {α : Type u_1} (l : List α) (n : Nat) : l.toArray.take n = (List.take n l).toArray

@[simp]

theorem List.mapM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) : Array.mapM f l.toArray = List.toArray <$> List.mapM f l

@[simp]

theorem List.map_toArray {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : Array.map f l.toArray = (List.map f l).toArray

@[simp]

theorem List.set_toArray {α : Type u_1} (l : List α) (i : Fin l.toArray.size) (a : α) : l.toArray.set (↑i) a ⋯ = (l.set (↑i) a).toArray

@[simp]

theorem List.uset_toArray {α : Type u_1} (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) : l.toArray.uset i a h = (l.set i.toNat a).toArray

@[simp]

theorem List.setIfInBounds_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) : l.toArray.setIfInBounds i a = (l.set i a).toArray

theorem List.anyM_toArray {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) : Array.anyM p l.toArray = List.anyM p l

theorem List.any_toArray {α : Type u_1} (p : α → Bool) (l : List α) : l.toArray.any p = l.any p

theorem List.allM_toArray {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) : Array.allM p l.toArray = List.allM p l

theorem List.all_toArray {α : Type u_1} (p : α → Bool) (l : List α) : l.toArray.all p = l.all p

@[simp]

theorem List.anyM_toArray' {m : Type → Type u_1} {α : Type u_2} {stop : Nat} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) (h : stop = l.toArray.size) : Array.anyM p l.toArray 0 stop = List.anyM p l

Variant of anyM_toArray with a side condition on stop.

@[simp]

theorem List.any_toArray' {α : Type u_1} {stop : Nat} (p : α → Bool) (l : List α) (h : stop = l.toArray.size) : l.toArray.any p 0 stop = l.any p

Variant of any_toArray with a side condition on stop.

@[simp]

theorem List.allM_toArray' {m : Type → Type u_1} {α : Type u_2} {stop : Nat} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) (h : stop = l.toArray.size) : Array.allM p l.toArray 0 stop = List.allM p l

Variant of allM_toArray with a side condition on stop.

@[simp]

theorem List.all_toArray' {α : Type u_1} {stop : Nat} (p : α → Bool) (l : List α) (h : stop = l.toArray.size) : l.toArray.all p 0 stop = l.all p

Variant of all_toArray with a side condition on stop.

@[simp]

theorem List.swap_toArray {α : Type u_1} (l : List α) (i j : Nat) {hi : i < l.toArray.size} {hj : j < l.toArray.size} : l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray

@[simp]

theorem List.reverse_toArray {α : Type u_1} (l : List α) : l.toArray.reverse = l.reverse.toArray

@[simp]

theorem List.modify_toArray {α : Type u_1} {i : Nat} (f : α → α) (l : List α) : l.toArray.modify i f = (List.modify f i l).toArray

@[simp]

theorem List.filter_toArray' {α : Type u_1} {stop : Nat} (p : α → Bool) (l : List α) (h : stop = l.toArray.size) : Array.filter p l.toArray 0 stop = (List.filter p l).toArray

@[simp]

theorem List.filterMap_toArray' {α : Type u_1} {β : Type u_2} {stop : Nat} (f : α → Option β) (l : List α) (h : stop = l.toArray.size) : Array.filterMap f l.toArray 0 stop = (List.filterMap f l).toArray

theorem List.filter_toArray {α : Type u_1} (p : α → Bool) (l : List α) : Array.filter p l.toArray = (List.filter p l).toArray

theorem List.filterMap_toArray {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : Array.filterMap f l.toArray = (List.filterMap f l).toArray

@[simp]

theorem List.flatten_toArray {α : Type u_1} (l : List (List α)) : (Array.map List.toArray l.toArray).flatten = l.flatten.toArray

@[simp]

theorem List.toArray_range (n : Nat) : (List.range n).toArray = Array.range n

@[simp]

theorem List.extract_toArray {α : Type u_1} (l : List α) (start stop : Nat) : l.toArray.extract start stop = (List.take (stop - start) (List.drop start l)).toArray

@[simp]

theorem List.toArray_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (List.ofFn f).toArray = Array.ofFn f

@[simp, irreducible]

theorem List.eraseIdx_toArray {α : Type u_1} (l : List α) (i : Nat) (h : i < l.toArray.size) : l.toArray.eraseIdx i h = (l.eraseIdx i).toArray

@[simp]

theorem List.eraseIdxIfInBounds_toArray {α : Type u_1} (l : List α) (i : Nat) : l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray

@[simp]

theorem Array.mapM_id {α : Type u_1} {β : Type u_2} {l : Array α} {f : α → Id β} : Array.mapM f l = Array.map f l

@[simp]

theorem Array.toList_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f

@[simp]

theorem Array.toList_takeWhile {α : Type u_1} (p : α → Bool) (as : Array α) : (Array.takeWhile p as).toList = List.takeWhile p as.toList

@[simp]

theorem Array.toList_eraseIdx {α : Type u_1} (as : Array α) (i : Nat) (h : i < as.size) : (as.eraseIdx i h).toList = as.toList.eraseIdx i

@[simp]

theorem Array.toList_eraseIdxIfInBounds {α : Type u_1} (as : Array α) (i : Nat) : (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i

map

@[simp]

theorem Array.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {as : Array α} : Array.map g (Array.map f as) = Array.map (g ∘ f) as

@[simp]

theorem Array.map_id_fun {α : Type u_1} : Array.map id = id

@[simp]

theorem Array.map_id_fun' {α : Type u_1} : (Array.map fun (a : α) => a) = id

map_id_fun' differs from map_id_fun by representing the identity function as a lambda, rather than id.

theorem Array.map_id {α : Type u_1} (as : Array α) : Array.map id as = as

theorem Array.map_id' {α : Type u_1} (as : Array α) : Array.map (fun (a : α) => a) as = as

map_id' differs from map_id by representing the identity function as a lambda, rather than id.

theorem Array.map_id'' {α : Type u_1} {f : α → α} (h : ∀ (x : α), f x = x) (as : Array α) : Array.map f as = as

Variant of map_id, with a side condition that the function is pointwise the identity.

theorem Array.array_array_induction {α : Type u_1} (P : Array (Array α) → Prop) (h : ∀ (xss : List (List α)), P (List.map List.toArray xss).toArray) (ass : Array (Array α)) : P ass

theorem Array.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) : Array.foldl g init (Array.map f l) = Array.foldl (fun (x : α) (y : β₁) => g x (f y)) init l

theorem Array.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g : α₂ → β → β) (l : Array α₁) (init : β) : Array.foldr g init (Array.map f l) = Array.foldr (fun (x : α₁) (y : β) => g (f x) y) init l

theorem Array.foldl_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : γ → β → γ) (l : Array α) (init : γ) : Array.foldl g init (Array.filterMap f l) = Array.foldl (fun (x : γ) (y : α) => match f y with | some b => g x b | none => x) init l

theorem Array.foldr_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → γ → γ) (l : Array α) (init : γ) : Array.foldr g init (Array.filterMap f l) = Array.foldr (fun (x : α) (y : γ) => match f x with | some b => g b y | none => y) init l

theorem Array.foldl_map' {α : Type u_1} {β : Type u_2} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Array α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : Array.foldl f' (g a) (Array.map g l) = g (Array.foldl f a l)

theorem Array.foldr_map' {α : Type u_1} {β : Type u_2} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)

flatten

@[simp]

theorem Array.flatten_empty {α : Type u_1} : #[].flatten = #[]

@[simp]

theorem Array.flatten_toArray_map_toArray {α : Type u_1} (xss : List (List α)) : (List.map List.toArray xss).toArray.flatten = xss.flatten.toArray

reverse

@[simp]

theorem Array.mem_reverse {α : Type u_1} {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as

findSomeRevM?, findRevM?, findSomeRev?, findRev?

@[simp]

theorem Array.findSomeRevM?_eq_findSomeM?_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m (Option β)) (as : Array α) : Array.findSomeRevM? f as = Array.findSomeM? f as.reverse

@[simp]

theorem Array.findRevM?_eq_findM?_reverse {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (as : Array α) : Array.findRevM? f as = Array.findM? f as.reverse

@[simp]

theorem Array.findSomeRev?_eq_findSome?_reverse {α : Type u_1} {β : Type u_2} (f : α → Option β) (as : Array α) : Array.findSomeRev? f as = Array.findSome? f as.reverse

@[simp]

theorem Array.findRev?_eq_find?_reverse {α : Type} (f : α → Bool) (as : Array α) : Array.findRev? f as = Array.find? f as.reverse

unzip

@[simp]

theorem Array.fst_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.fst = Array.map Prod.fst as

@[simp]

theorem Array.snd_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.snd = Array.map Prod.snd as

@[simp]

theorem List.unzip_toArray {α : Type u_1} {β : Type u_2} (as : List (α × β)) : as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip

@[simp]

theorem Array.toList_fst_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.fst.toList = as.toList.unzip.fst

@[simp]

theorem Array.toList_snd_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.snd.toList = as.toList.unzip.snd

@[simp]

theorem Array.flatMap_empty {α : Type u_1} {β : Type u_2} (f : α → Array β) : Array.flatMap f #[] = #[]

@[simp]

theorem Array.flatMap_toArray_cons {α : Type u_1} {β : Type u_2} (f : α → Array β) (a : α) (as : List α) : Array.flatMap f (a :: as).toArray = f a ++ Array.flatMap f as.toArray

@[simp]

theorem Array.flatMap_toArray {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : List α) : Array.flatMap f as.toArray = (as.flatMap fun (a : α) => (f a).toList).toArray

Deprecations

@[reducible, inline, deprecated List.toArray_toList]

abbrev List.toArray_data {α : Type u_1} (a : Array α) : a.toList.toArray = a

Equations

• @List.toArray_data = @List.toArray_toList

@[deprecated]

theorem List.toArray_concat {α : Type u_1} {as : List α} {x : α} : (as ++ [x]).toArray = as.toArray.push x

@[reducible, inline, deprecated List.back!_toArray]

abbrev List.back_toArray {α : Type u_1} [Inhabited α] (l : List α) : l.toArray.back! = l.getLast!

Equations

• @List.back_toArray = @List.back!_toArray

@[reducible, inline, deprecated List.setIfInBounds_toArray]

abbrev List.setD_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) : l.toArray.setIfInBounds i a = (l.set i a).toArray

Equations

• @List.setD_toArray = @List.setIfInBounds_toArray

@[reducible, inline, deprecated Array.getElem_eq_getElem_toList]

abbrev Array.getElem_eq_toList_getElem {α : Type u_1} {i : Nat} {a : Array α} (h : i < a.size) : a[i] = a.toList[i]

Equations

• @Array.getElem_eq_toList_getElem = @Array.getElem_eq_getElem_toList

@[reducible, inline, deprecated Array.getElem_eq_toList_getElem]

abbrev Array.getElem_eq_data_getElem {α : Type u_1} {i : Nat} {a : Array α} (h : i < a.size) : a[i] = a.toList[i]

Equations

• @Array.getElem_eq_data_getElem = @Array.getElem_eq_getElem_toList

@[deprecated Array.getElem_eq_toList_getElem]

theorem Array.getElem_eq_toList_get {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩

@[reducible, inline, deprecated Array.toArray_toList]

abbrev Array.toArray_data {α : Type u_1} (a : Array α) : a.toList.toArray = a

Equations

• @Array.toArray_data = @Array.toArray_toList

@[reducible, inline, deprecated Array.length_toList]

abbrev Array.data_length {α : Type u_1} {l : Array α} : l.toList.length = l.size

Equations

• @Array.data_length = @Array.length_toList

@[reducible, inline, deprecated Array.toList_map]

abbrev Array.map_data {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : (Array.map f arr).toList = List.map f arr.toList

Equations

• @Array.map_data = @Array.toList_map

@[reducible, inline, deprecated Array.foldl_toList_eq_flatMap]

abbrev Array.foldl_toList_eq_bind {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β) (H : ∀ (acc : Array β) (a : α), (F acc a).toList = acc.toList ++ G a) : (List.foldl F acc l).toList = acc.toList ++ l.flatMap G

Equations

• @Array.foldl_toList_eq_bind = @Array.foldl_toList_eq_flatMap

@[reducible, inline, deprecated Array.foldl_toList_eq_flatMap]

abbrev Array.foldl_data_eq_bind {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β) (H : ∀ (acc : Array β) (a : α), (F acc a).toList = acc.toList ++ G a) : (List.foldl F acc l).toList = acc.toList ++ l.flatMap G

Equations

• @Array.foldl_data_eq_bind = @Array.foldl_toList_eq_flatMap

@[reducible, inline, deprecated Array.foldl_toList_eq_map]

abbrev Array.foldl_data_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (G : α → β) : (List.foldl (fun (acc : Array β) (a : α) => acc.push (G a)) acc l).toList = acc.toList ++ List.map G l

Equations

• @Array.foldl_data_eq_map = @Array.foldl_toList_eq_map

@[reducible, inline, deprecated Array.toList_mkArray]

abbrev Array.mkArray_data {α : Type u_1} (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v

Equations

• @Array.mkArray_data = @Array.toList_mkArray

@[reducible, inline, deprecated Array.mem_toList]

abbrev Array.mem_data {α : Type u_1} {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l

Equations

• @Array.mem_data = @Array.mem_toList

@[reducible, inline, deprecated Array.getElem_mem]

abbrev Array.getElem?_mem {α : Type u_1} {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l

Equations

• @Array.getElem?_mem = @Array.getElem_mem

@[reducible, inline, deprecated Array.getElem_fin_eq_getElem_toList]

abbrev Array.getElem_fin_eq_toList_get {α : Type u_1} (a : Array α) (i : Fin a.size) : a[i] = a.toList[i]

Equations

• @Array.getElem_fin_eq_toList_get = @Array.getElem_fin_eq_getElem_toList

@[reducible, inline, deprecated Array.getElem_fin_eq_getElem_toList]

abbrev Array.getElem_fin_eq_data_get {α : Type u_1} (a : Array α) (i : Fin a.size) : a[i] = a.toList[i]

Equations

• @Array.getElem_fin_eq_data_get = @Array.getElem_fin_eq_getElem_toList

@[reducible, inline, deprecated Array.getElem_mem_toList]

abbrev Array.getElem_mem_data {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) : a[i] ∈ a.toList

Equations

• @Array.getElem_mem_data = @Array.getElem_mem_toList

@[reducible, inline, deprecated Array.getElem?_eq_getElem?_toList]

abbrev Array.getElem?_eq_toList_getElem? {α : Type u_1} (a : Array α) (i : Nat) : a[i]? = a.toList[i]?

Equations

• @Array.getElem?_eq_toList_getElem? = @Array.getElem?_eq_getElem?_toList

@[deprecated Array.getElem?_eq_toList_getElem?]

theorem Array.getElem?_eq_toList_get? {α : Type u_1} (a : Array α) (i : Nat) : a[i]? = a.toList.get? i

@[reducible, inline, deprecated Array.getElem?_eq_toList_getElem?]

abbrev Array.getElem?_eq_data_get? {α : Type u_1} (a : Array α) (i : Nat) : a[i]? = a.toList.get? i

Equations

• @Array.getElem?_eq_data_get? = @Array.getElem?_eq_toList_get?

@[reducible, inline, deprecated Array.get?_eq_get?_toList]

abbrev Array.get?_eq_toList_get? {α : Type u_1} (a : Array α) (i : Nat) : a.get? i = a.toList.get? i

Equations

• @Array.get?_eq_toList_get? = @Array.get?_eq_get?_toList

@[reducible, inline, deprecated Array.get?_eq_toList_get?]

abbrev Array.get?_eq_data_get? {α : Type u_1} (a : Array α) (i : Nat) : a.get? i = a.toList.get? i

Equations

• @Array.get?_eq_data_get? = @Array.get?_eq_get?_toList

@[reducible, inline, deprecated Array.toList_set]

abbrev Array.data_set {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size) : (a.set i v h).toList = a.toList.set i v

Equations

• @Array.data_set = @Array.toList_set

@[reducible, inline, deprecated Array.toList_swap]

abbrev Array.data_swap {α : Type u_1} (a : Array α) (i j : Nat) (hi : i < a.size) (hj : j < a.size) : (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i]

Equations

• @Array.data_swap = @Array.toList_swap

@[reducible, inline, deprecated Array.getElem?_swap]

abbrev Array.get?_swap {α : Type u_1} (a : Array α) (i j : Nat) (hi : i < a.size) (hj : j < a.size) (k : Nat) : (a.swap i j hi hj)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[k]?

Equations

• @Array.get?_swap = @Array.getElem?_swap

@[reducible, inline, deprecated Array.toList_pop]

abbrev Array.data_pop {α : Type u_1} (a : Array α) : a.pop.toList = a.toList.dropLast

Equations

• @Array.data_pop = @Array.toList_pop

@[reducible, inline, deprecated Array.size_eq_length_toList]

abbrev Array.size_eq_length_data {α : Type u_1} (as : Array α) : as.size = as.toList.length

Equations

• @Array.size_eq_length_data = @Array.size_eq_length_toList

@[reducible, inline, deprecated Array.toList_range]

abbrev Array.data_range (n : Nat) : (Array.range n).toList = List.range n

Equations

• Array.data_range = Array.toList_range

@[reducible, inline, deprecated Array.toList_reverse]

abbrev Array.reverse_toList {α : Type u_1} (a : Array α) : a.reverse.toList = a.toList.reverse

Equations

• @Array.reverse_toList = @Array.toList_reverse

@[reducible, inline, deprecated Array.mapM_eq_mapM_toList]

abbrev Array.mapM_eq_mapM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : Array.mapM f arr = List.toArray <$> List.mapM f arr.toList

Equations

• @Array.mapM_eq_mapM_data = @Array.mapM_eq_mapM_toList

@[deprecated Array.getElem_modify]

theorem Array.get_modify {α : Type u_1} {f : α → α} {arr : Array α} {x i : Nat} (h : i < (arr.modify x f).size) : (arr.modify x f).get i h = if x = i then f (arr.get i ⋯) else arr.get i ⋯

@[reducible, inline, deprecated Array.toList_filter]

abbrev Array.filter_data {α : Type u_1} (p : α → Bool) (l : Array α) : (Array.filter p l).toList = List.filter p l.toList

Equations

• @Array.filter_data = @Array.toList_filter

@[reducible, inline, deprecated Array.toList_filterMap]

abbrev Array.filterMap_data {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : Array α) : (Array.filterMap f l).toList = List.filterMap f l.toList

Equations

• @Array.filterMap_data = @Array.toList_filterMap

@[reducible, inline, deprecated Array.toList_empty]

abbrev Array.empty_data {α : Type u_1} : #[].toList = []

Equations

• @Array.empty_data = @Array.toList_empty

@[reducible, inline, deprecated Array.getElem_append_left]

abbrev Array.get_append_left {α : Type u_1} {i : Nat} {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) : (as ++ bs)[i] = as[i]

Equations

• @Array.get_append_left = @Array.getElem_append_left

@[reducible, inline, deprecated Array.getElem_append_right]

abbrev Array.get_append_right {α : Type u_1} {i : Nat} {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) (hlt : i - as.size < bs.size := ⋯) : (as ++ bs)[i] = bs[i - as.size]

Equations

• @Array.get_append_right = @Array.getElem_append_right

@[reducible, inline, deprecated]

abbrev Array.any_def {α : Type u_1} {p : α → Bool} (as : Array α) : as.toList.any p = as.any p

Equations

• @Array.any_def = @Array.any_toList

@[reducible, inline, deprecated]

abbrev Array.all_def {α : Type u_1} {p : α → Bool} (as : Array α) : as.toList.all p = as.all p

Equations

• @Array.all_def = @Array.all_toList

@[reducible, inline, deprecated Array.getElem_extract_loop_lt_aux]

abbrev Array.get_extract_loop_lt_aux {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hlt : i < bs.size) : i < (Array.extract.loop as size start bs).size

Equations

• @Array.get_extract_loop_lt_aux = @Array.getElem_extract_loop_lt_aux

@[reducible, inline, deprecated Array.getElem_extract_loop_lt]

abbrev Array.get_extract_loop_lt {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hlt : i < bs.size) (h : i < (Array.extract.loop as size start bs).size := ⋯) : (Array.extract.loop as size start bs)[i] = bs[i]

Equations

• @Array.get_extract_loop_lt = @Array.getElem_extract_loop_lt

@[reducible, inline, deprecated Array.getElem_extract_loop_ge_aux]

abbrev Array.get_extract_loop_ge_aux {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size) (h : i < (Array.extract.loop as size start bs).size) : start + i - bs.size < as.size

Equations

• @Array.get_extract_loop_ge_aux = @Array.getElem_extract_loop_ge_aux

@[reducible, inline, deprecated Array.getElem_extract_loop_ge]

abbrev Array.get_extract_loop_ge {α : Type u_1} {i : Nat} (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size) (h : i < (Array.extract.loop as size start bs).size) (h' : start + i - bs.size < as.size := ⋯) : (Array.extract.loop as size start bs)[i] = as[start + i - bs.size]

Equations

• @Array.get_extract_loop_ge = @Array.getElem_extract_loop_ge

@[reducible, inline, deprecated Array.getElem_extract_aux]

abbrev Array.get_extract_aux {α : Type u_1} {i : Nat} {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) : start + i < as.size

Equations

• @Array.get_extract_aux = @Array.getElem_extract_aux

@[reducible, inline, deprecated Array.getElem_extract]

abbrev Array.get_extract {α : Type u_1} {i : Nat} {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) : (as.extract start stop)[i] = as[start + i]

Equations

• @Array.get_extract = @Array.getElem_extract

@[reducible, inline, deprecated Array.getElem_swap_right]

abbrev Array.get_swap_right {α : Type u_1} (a : Array α) {i j : Nat} {hi : i < a.size} {hj : j < a.size} : (a.swap i j hi hj)[j] = a[i]

Equations

• @Array.get_swap_right = @Array.getElem_swap_right

@[reducible, inline, deprecated Array.getElem_swap_left]

abbrev Array.get_swap_left {α : Type u_1} (a : Array α) {i j : Nat} {hi : i < a.size} {hj : j < a.size} : (a.swap i j hi hj)[i] = a[j]

Equations

• @Array.get_swap_left = @Array.getElem_swap_left

@[reducible, inline, deprecated Array.getElem_swap_of_ne]

abbrev Array.get_swap_of_ne {α : Type u_1} {p : Nat} (a : Array α) {i j : Nat} {hi : i < a.size} {hj : j < a.size} (hp : p < a.size) (hi' : p ≠ i) (hj' : p ≠ j) : (a.swap i j hi hj)[p] = a[p]

Equations

• @Array.get_swap_of_ne = @Array.getElem_swap_of_ne

@[reducible, inline, deprecated Array.getElem_swap]

abbrev Array.get_swap {α : Type u_1} (a : Array α) (i j : Nat) {hi : i < a.size} {hj : j < a.size} (k : Nat) (hk : k < (a.swap i j hi hj).size) : (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

Equations

• @Array.get_swap = @Array.getElem_swap

@[reducible, inline, deprecated Array.getElem_swap']

abbrev Array.get_swap' {α : Type u_1} (a : Array α) (i j : Nat) {hi : i < a.size} {hj : j < a.size} (k : Nat) (hk : k < a.size) : (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

Equations

• @Array.get_swap' = @Array.getElem_swap'

@[reducible, inline, deprecated Array.back!_eq_back?]

abbrev Array.back_eq_back? {α : Type u_1} [Inhabited α] (a : Array α) : a.back! = a.back?.getD default

Equations

• @Array.back_eq_back? = @Array.back!_eq_back?

@[reducible, inline, deprecated Array.back!_push]

abbrev Array.back_push {α : Type u_1} {x : α} [Inhabited α] (a : Array α) : (a.push x).back! = x

Equations

• @Array.back_push = @Array.back!_push

@[reducible, inline, deprecated Array.eq_push_pop_back!_of_size_ne_zero]

abbrev Array.eq_push_pop_back_of_size_ne_zero {α : Type u_1} [Inhabited α] {as : Array α} (h : as.size ≠ 0) : as = as.pop.push as.back!

Equations

• @Array.eq_push_pop_back_of_size_ne_zero = @Array.eq_push_pop_back!_of_size_ne_zero

@[reducible, inline, deprecated Array.set!_is_setIfInBounds]

abbrev Array.set_is_setIfInBounds : @Array.set! = @Array.setIfInBounds

Equations

• Array.set_is_setIfInBounds = Array.set!_is_setIfInBounds

@[reducible, inline, deprecated Array.size_setIfInBounds]

abbrev Array.size_setD {α : Type u_1} (a : Array α) (index : Nat) (val : α) : (a.setIfInBounds index val).size = a.size

Equations

• @Array.size_setD = @Array.size_setIfInBounds

@[reducible, inline, deprecated Array.getElem_setIfInBounds_eq]

abbrev Array.getElem_setD_eq {α : Type u_1} (a : Array α) {i : Nat} (v : α) (h : i < (a.setIfInBounds i v).size) : (a.setIfInBounds i v)[i] = v

Equations

• @Array.getElem_setD_eq = @Array.getElem_setIfInBounds_eq

@[reducible, inline, deprecated Array.getElem?_setIfInBounds_eq]

abbrev Array.get?_setD_eq {α : Type u_1} (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setIfInBounds i v)[i]? = some v

Equations

• @Array.get?_setD_eq = @Array.getElem?_setIfInBounds_eq

@[reducible, inline, deprecated Array.getD_get?_setIfInBounds]

abbrev Array.getD_setD {α : Type u_1} (a : Array α) (i : Nat) (v d : α) : (a.setIfInBounds i v)[i]?.getD d = if i < a.size then v else d

Equations

• @Array.getD_setD = @Array.getD_get?_setIfInBounds

@[reducible, inline, deprecated Array.getElem_setIfInBounds]

abbrev Array.getElem_setD {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < (a.setIfInBounds i v).size) : (a.setIfInBounds i v)[i] = v

Equations

• @Array.getElem_setD = @Array.getElem_setIfInBounds