Documentation

Init.Data.List.ToArray

Lemmas about List.toArray. #

We prefer to pull List.toArray outwards past Array operations.

source
@[simp]
theorem Array.toList_set {α : Type u_1} (a : Array α) (i : Nat) (x : α) (h : i < a.size) :
(a.set i x h).toList = a.toList.set i x
source
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] ⋯
source
@[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]
source
theorem List.toArray_inj {α : Type u_1} {a b : List α} (h : a.toArray = b.toArray) :
a = b
source
@[simp]
theorem List.size_toArrayAux {α : Type u_1} {a : List α} {b : Array α} :
(a.toArrayAux b).size = b.size + a.length
source
theorem List.toArray_cons {α : Type u_1} (a : α) (l : List α) :
(a :: l).toArray = #[a] ++ l.toArray
source
@[simp]
theorem List.push_toArray {α : Type u_1} (l : List α) (a : α) :
l.toArray.push a = (l ++ [a]).toArray
source
@[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.

source
@[simp]
theorem List.isEmpty_toArray {α : Type u_1} (l : List α) :
l.toArray.isEmpty = l.isEmpty
source
@[simp]
theorem List.toArray_singleton {α : Type u_1} (a : α) :
(List.singleton a).toArray = Array.singleton a
source
@[simp]
theorem List.back!_toArray {α : Type u_1} [Inhabited α] (l : List α) :
l.toArray.back! = l.getLast!
source
@[simp]
theorem List.back?_toArray {α : Type u_1} (l : List α) :
l.toArray.back? = l.getLast?
source
@[simp]
theorem List.set_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) (h : i < l.length) :
l.toArray.set i a h = (l.set i a).toArray
source
@[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' (drop (l.length - i) l) b fun (a : α) (m : a ∈ drop (l.length - i) l) (b : β) => f a ⋯ b
source
@[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
source
@[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
source
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 = foldrM f init l
source
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
source
theorem List.foldr_toArray {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (l : List α) :
Array.foldr f init l.toArray = foldr f init l
source
theorem List.foldl_toArray {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (l : List α) :
Array.foldl f init l.toArray = foldl f init l
source
@[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 = foldrM f init l

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

source
@[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.

source
@[simp]
theorem List.forM_toArray' {m : Type u_1 → Type u_2} {α : Type u_3} {stop : Nat} [Monad m] (l : List α) (f : α → m PUnit) (h : stop = l.toArray.size) :
Array.forM f l.toArray 0 stop = l.forM f

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

source
@[simp]
theorem List.forM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (l : List α) (f : α → m PUnit) :
forM l.toArray f = l.forM f
source
@[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 = foldr f init l

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

source
@[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 = foldl f init l

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

source
@[simp]
theorem List.sum_toArray {α : Type u_1} [Add α] [Zero α] (l : List α) :
l.toArray.sum = l.sum
source
@[simp]
theorem List.append_toArray {α : Type u_1} (l₁ l₂ : List α) :
l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray
source
@[simp]
theorem List.push_append_toArray {α : Type u_1} {as : Array α} {a : α} {bs : List α} :
as.push a ++ bs.toArray = as ++ (a :: bs).toArray
source
@[simp]
theorem List.foldl_push {α : Type u_1} {l : List α} {as : Array α} :
foldl Array.push as l = as ++ l.toArray
source
@[simp]
theorem List.foldr_push {α : Type u_1} {l : List α} {as : Array α} :
foldr (fun (a : α) (b : Array α) => b.push a) as l = as ++ l.reverse.toArray
source
@[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 = findSomeM? f l
source
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 = findSomeM? f (take i l).reverse
source
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 = findSomeM? f l.reverse
source
theorem List.findRevM?_toArray {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
Array.findRevM? f l.toArray = findM? f l.reverse
source
@[simp]
theorem List.findM?_toArray {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
Array.findM? f l.toArray = findM? f l
source
@[simp]
theorem List.findSome?_toArray {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) :
Array.findSome? f l.toArray = findSome? f l
source
@[simp]
theorem List.find?_toArray {α : Type u_1} (f : α → Bool) (l : List α) :
Array.find? f l.toArray = find? f l
source
@[simp]
theorem List.findFinIdx?_toArray {α : Type u_1} (p : α → Bool) (l : List α) :
Array.findFinIdx? p l.toArray = findFinIdx? p l
source
@[simp]
theorem List.findIdx?_toArray {α : Type u_1} (p : α → Bool) (l : List α) :
Array.findIdx? p l.toArray = findIdx? p l
source
@[simp]
theorem List.finIdxOf?_toArray {α : Type u_1} [BEq α] (a : α) (l : List α) :
l.toArray.finIdxOf? a = finIdxOf? a l
source
@[simp]
theorem List.idxOf?_toArray {α : Type u_1} [BEq α] (a : α) (l : List α) :
l.toArray.idxOf? a = idxOf? a l
source
@[simp]
theorem List.findIdx_toArray {α : Type u_1} {as : List α} {p : α → Bool} :
Array.findIdx p as.toArray = findIdx p as
source
@[simp]
theorem List.idxOf_toArray {α : Type u_1} [BEq α] {as : List α} {a : α} :
Array.idxOf a as.toArray = idxOf a as
source
@[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
source
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) = (drop (i + 1) l₁).toArray.isPrefixOfAux (drop (i + 1) l₂).toArray ⋯ 0
source
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₂
source
@[simp]
theorem List.isPrefixOf_toArray {α : Type u_1} [BEq α] (l₁ l₂ : List α) :
l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂
source
@[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
source
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 = (drop (i + 1) as).toArray.zipWithAux (drop (i + 1) bs).toArray f 0 cs
source
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 ++ (zipWith f as bs).toArray
source
@[simp]
theorem List.zipWith_toArray {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : α → β → γ) :
Array.zipWith f as.toArray bs.toArray = (zipWith f as bs).toArray
source
@[simp]
theorem List.zip_toArray {α : Type u_1} {β : Type u_2} (as : List α) (bs : List β) :
as.toArray.zip bs.toArray = (as.zip bs).toArray
source
@[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 ++ (zipWithAll f (drop i as) (drop i bs)).toArray
source
@[simp]
theorem List.zipWithAll_toArray {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) (as : List α) (bs : List β) :
Array.zipWithAll f as.toArray bs.toArray = (zipWithAll f as bs).toArray
source
@[simp]
theorem List.toArray_appendList {α : Type u_1} (l₁ l₂ : List α) :
l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray
source
@[simp]
theorem List.pop_toArray {α : Type u_1} (l : List α) :
l.toArray.pop = l.dropLast.toArray
source
@[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
source
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 ++ (takeWhile p (drop i l)).toArray
source
@[simp]
theorem List.takeWhile_toArray {α : Type u_1} (p : α → Bool) (l : List α) :
Array.takeWhile p l.toArray = (takeWhile p l).toArray
source
@[simp]
theorem List.setIfInBounds_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) :
l.toArray.setIfInBounds i a = (l.set i a).toArray
source
@[simp]
theorem List.toArray_replicate {α : Type u_1} (n : Nat) (v : α) :
(replicate n v).toArray = mkArray n v
source
@[reducible, inline, deprecated List.toArray_replicate (since := "2024-12-13")]
abbrev Array.mkArray_eq_toArray_replicate {α : Type u_1} (n : Nat) (v : α) :
(List.replicate n v).toArray = mkArray n v
Equations
Instances For
    source
    @[simp]
    theorem List.flatMap_empty {α : Type u_1} {β : Type u_2} (f : α → Array β) :
    Array.flatMap f #[] = #[]
    source
    theorem List.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
    source
    @[simp]
    theorem List.flatMap_toArray {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : List α) :
    Array.flatMap f as.toArray = (flatMap (fun (a : α) => (f a).toList) as).toArray
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem List.eraseIdxIfInBounds_toArray {α : Type u_1} (l : List α) (i : Nat) :
    l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray
    source
    @[simp]
    theorem List.eraseP_toArray {α : Type u_1} {as : List α} {p : α → Bool} :
    as.toArray.eraseP p = (eraseP p as).toArray
    source
    @[simp]
    theorem List.erase_toArray {α : Type u_1} [BEq α] {as : List α} {a : α} :
    as.toArray.erase a = (as.erase a).toArray