theorem Vector.toArray_injective {α : Type u_1} {n : Nat} {v w : Vector α n} : v.toArray = w.toArray → v = w

theorem Vector.ext {α : Type u_1} {n : Nat} {a b : Vector α n} (h : ∀ (i : Nat) (x : i < n), a[i] = b[i]) : a = b

mk lemmas

theorem Vector.toArray_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.toArray = a

@[simp]

theorem Vector.allDiff_mk {α : Type u_1} {n : Nat} [BEq α] (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.allDiff = a.allDiff

@[simp]

theorem Vector.mk_append_mk {α : Type u_1} {n m : Nat} (a b : Array α) (ha : a.size = n) (hb : b.size = m) : { toArray := a, size_toArray := ha } ++ { toArray := b, size_toArray := hb } = { toArray := a ++ b, size_toArray := ⋯ }

@[simp]

theorem Vector.back!_mk {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.back! = a.back!

@[simp]

theorem Vector.back?_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.back? = a.back?

@[simp]

theorem Vector.drop_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (m : Nat) : { toArray := a, size_toArray := h }.drop m = { toArray := a.extract m a.size, size_toArray := ⋯ }

@[simp]

theorem Vector.eraseIdx_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (h' : i < n) : { toArray := a, size_toArray := h }.eraseIdx i h' = { toArray := a.eraseIdx i ⋯, size_toArray := ⋯ }

@[simp]

theorem Vector.eraseIdx!_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (hi : i < n) : { toArray := a, size_toArray := h }.eraseIdx! i = { toArray := a.eraseIdx i ⋯, size_toArray := ⋯ }

@[simp]

theorem Vector.extract_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (start stop : Nat) : { toArray := a, size_toArray := h }.extract start stop = { toArray := a.extract start stop, size_toArray := ⋯ }

@[simp]

theorem Vector.getElem_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (hi : i < n) : { toArray := a, size_toArray := h }[i] = a[i]

@[simp]

theorem Vector.get_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) : { toArray := a, size_toArray := h }.get i = a[i]

@[simp]

theorem Vector.getD_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : { toArray := a, size_toArray := h }.getD i x = a.getD i x

@[simp]

theorem Vector.uget_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : USize) (hi : i.toNat < n) : { toArray := a, size_toArray := h }.uget i hi = a.uget i ⋯

@[simp]

theorem Vector.indexOf?_mk {α : Type u_1} {n : Nat} [BEq α] (a : Array α) (h : a.size = n) (x : α) : { toArray := a, size_toArray := h }.indexOf? x = Option.map (Fin.cast h) (a.indexOf? x)

@[simp]

theorem Vector.mk_isEqv_mk {α : Type u_1} {n : Nat} (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) : { toArray := a, size_toArray := ha }.isEqv { toArray := b, size_toArray := hb } r = a.isEqv b r

@[simp]

theorem Vector.mk_isPrefixOf_mk {α : Type u_1} {n m : Nat} [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = m) : { toArray := a, size_toArray := ha }.isPrefixOf { toArray := b, size_toArray := hb } = a.isPrefixOf b

@[simp]

theorem Vector.map_mk {α : Type u_1} {n : Nat} {β : Type u_2} (a : Array α) (h : a.size = n) (f : α → β) : map f { toArray := a, size_toArray := h } = { toArray := Array.map f a, size_toArray := ⋯ }

@[simp]

theorem Vector.pop_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.pop = { toArray := a.pop, size_toArray := ⋯ }

@[simp]

theorem Vector.push_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (x : α) : push x { toArray := a, size_toArray := h } = { toArray := a.push x, size_toArray := ⋯ }

@[simp]

theorem Vector.reverse_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) : { toArray := a, size_toArray := h }.reverse = { toArray := a.reverse, size_toArray := ⋯ }

@[simp]

theorem Vector.set_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (w : i < n) : { toArray := a, size_toArray := h }.set i x w = { toArray := a.set i x ⋯, size_toArray := ⋯ }

@[simp]

theorem Vector.set!_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : { toArray := a, size_toArray := h }.set! i x = { toArray := a.set! i x, size_toArray := ⋯ }

@[simp]

theorem Vector.setIfInBounds_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : { toArray := a, size_toArray := h }.setIfInBounds i x = { toArray := a.setIfInBounds i x, size_toArray := ⋯ }

@[deprecated Vector.set_mk (since := "2024-11-25")]

theorem Vector.setN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (w : i < n) : { toArray := a, size_toArray := h }.set i x w = { toArray := a.set i x ⋯, size_toArray := ⋯ }

Alias of Vector.set_mk.

@[simp]

theorem Vector.swap_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) (hi : j < n) (hj : i < n) : { toArray := a, size_toArray := h }.swap i j hj hi = { toArray := a.swap i j ⋯ ⋯, size_toArray := ⋯ }

@[simp]

theorem Vector.swapIfInBounds_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) : { toArray := a, size_toArray := h }.swapIfInBounds i j = { toArray := a.swapIfInBounds i j, size_toArray := ⋯ }

@[deprecated Vector.swap_mk (since := "2024-11-25")]

theorem Vector.swapN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) (hi : j < n) (hj : i < n) : { toArray := a, size_toArray := h }.swap i j hj hi = { toArray := a.swap i j ⋯ ⋯, size_toArray := ⋯ }

Alias of Vector.swap_mk.

@[simp]

theorem Vector.swapAt_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (hi : i < n) : { toArray := a, size_toArray := h }.swapAt i x hi = ((a.swapAt i x ⋯).fst, { toArray := (a.swapAt i x ⋯).snd, size_toArray := ⋯ })

@[simp]

theorem Vector.swapAt!_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : { toArray := a, size_toArray := h }.swapAt! i x = ((a.swapAt! i x).fst, { toArray := (a.swapAt! i x).snd, size_toArray := ⋯ })

@[deprecated Vector.swapAt_mk (since := "2024-11-25")]

theorem Vector.swapAtN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (hi : i < n) : { toArray := a, size_toArray := h }.swapAt i x hi = ((a.swapAt i x ⋯).fst, { toArray := (a.swapAt i x ⋯).snd, size_toArray := ⋯ })

Alias of Vector.swapAt_mk.

@[simp]

theorem Vector.take_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (m : Nat) : { toArray := a, size_toArray := h }.take m = { toArray := a.take m, size_toArray := ⋯ }

@[simp]

theorem Vector.mk_zipWith_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} (f : α → β → γ) (a : Array α) (b : Array β) (ha : a.size = n) (hb : b.size = n) : { toArray := a, size_toArray := ha }.zipWith { toArray := b, size_toArray := hb } f = { toArray := a.zipWith b f, size_toArray := ⋯ }

@[simp]

theorem Vector.getElem_toArray {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (h : i < xs.size) : xs.toArray[i] = xs[i]

toArray lemmas

@[simp]

theorem Vector.toArray_append {α : Type u_1} {m n : Nat} (a : Vector α m) (b : Vector α n) : (a ++ b).toArray = a.toArray ++ b.toArray

@[simp]

theorem Vector.toArray_drop {α : Type u_1} {n : Nat} (a : Vector α n) (m : Nat) : (a.drop m).toArray = a.extract m a.size

@[simp]

theorem Vector.toArray_empty {α : Type u_1} : { toArray := #[], size_toArray := ⋯ }.toArray = #[]

@[simp]

theorem Vector.toArray_mkEmpty {α : Type u_1} (cap : Nat) : (mkEmpty cap).toArray = Array.mkEmpty cap

@[simp]

theorem Vector.toArray_eraseIdx {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (h : i < n) : (a.eraseIdx i h).toArray = a.eraseIdx i ⋯

@[simp]

theorem Vector.toArray_eraseIdx! {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (hi : i < n) : (a.eraseIdx! i).toArray = a.eraseIdx! i

@[simp]

theorem Vector.toArray_extract {α : Type u_1} {n : Nat} (a : Vector α n) (start stop : Nat) : (a.extract start stop).toArray = a.extract start stop

@[simp]

theorem Vector.toArray_map {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → β) (a : Vector α n) : (map f a).toArray = Array.map f a.toArray

@[simp]

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

@[simp]

theorem Vector.toArray_pop {α : Type u_1} {n : Nat} (a : Vector α n) : a.pop.toArray = a.pop

@[simp]

theorem Vector.toArray_push {α : Type u_1} {n : Nat} (a : Vector α n) (x : α) : (push x a).toArray = a.push x

@[simp]

theorem Vector.toArray_range {n : Nat} : (range n).toArray = Array.range n

@[simp]

theorem Vector.toArray_reverse {α : Type u_1} {n : Nat} (a : Vector α n) : a.reverse.toArray = a.reverse

@[simp]

theorem Vector.toArray_set {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) : (a.set i x h).toArray = a.set i x ⋯

@[simp]

theorem Vector.toArray_set! {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) : (a.set! i x).toArray = a.set! i x

@[simp]

theorem Vector.toArray_setIfInBounds {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) : (a.setIfInBounds i x).toArray = a.setIfInBounds i x

@[deprecated Vector.toArray_setIfInBounds (since := "2024-11-25")]

theorem Vector.toArray_setD {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) : (a.setIfInBounds i x).toArray = a.setIfInBounds i x

Alias of Vector.toArray_setIfInBounds.

@[deprecated Vector.toArray_set (since := "2024-11-25")]

theorem Vector.toArray_setN {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) : (a.set i x h).toArray = a.set i x ⋯

Alias of Vector.toArray_set.

@[simp]

theorem Vector.toArray_singleton {α : Type u_1} (x : α) : (singleton x).toArray = #[x]

@[simp]

theorem Vector.toArray_swap {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) (hi : j < n) (hj : i < n) : (a.swap i j hj hi).toArray = a.swap i j ⋯ ⋯

@[simp]

theorem Vector.toArray_swapIfInBounds {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) : (a.swapIfInBounds i j).toArray = a.swapIfInBounds i j

@[deprecated Vector.toArray_swapIfInBounds (since := "2024-11-25")]

theorem Vector.toArray_swap! {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) : (a.swapIfInBounds i j).toArray = a.swapIfInBounds i j

Alias of Vector.toArray_swapIfInBounds.

@[deprecated Vector.toArray_swap (since := "2024-11-25")]

theorem Vector.toArray_swapN {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) (hi : j < n) (hj : i < n) : (a.swap i j hj hi).toArray = a.swap i j ⋯ ⋯

Alias of Vector.toArray_swap.

@[simp]

theorem Vector.toArray_swapAt {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) : ((a.swapAt i x h).fst, (a.swapAt i x h).snd.toArray) = ((a.swapAt i x ⋯).fst, (a.swapAt i x ⋯).snd)

@[simp]

theorem Vector.toArray_swapAt! {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) : ((a.swapAt! i x).fst, (a.swapAt! i x).snd.toArray) = ((a.swapAt! i x).fst, (a.swapAt! i x).snd)

@[deprecated Vector.toArray_swapAt (since := "2024-11-25")]

theorem Vector.toArray_swapAtN {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) : ((a.swapAt i x h).fst, (a.swapAt i x h).snd.toArray) = ((a.swapAt i x ⋯).fst, (a.swapAt i x ⋯).snd)

Alias of Vector.toArray_swapAt.

@[simp]

theorem Vector.toArray_take {α : Type u_1} {n : Nat} (a : Vector α n) (m : Nat) : (a.take m).toArray = a.take m

@[simp]

theorem Vector.toArray_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} (f : α → β → γ) (a : Vector α n) (b : Vector β n) : (a.zipWith b f).toArray = a.zipWith b.toArray f

toList lemmas

theorem Vector.length_toList {α : Type u_1} {n : Nat} (xs : Vector α n) : xs.toList.length = n

theorem Vector.getElem_toList {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) : xs.toList[i] = xs[i]

getElem lemmas

@[simp]

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

@[simp]

theorem Vector.getElem_push_last {α : Type u_1} {n : Nat} {v : Vector α n} {x : α} : (push x v)[n] = x

@[simp]

theorem Vector.getElem_push_lt {α : Type u_1} {n : Nat} {v : Vector α n} {x : α} {i : Nat} (h : i < n) : (push x v)[i] = v[i]

@[simp]

theorem Vector.getElem_pop {α : Type u_1} {n : Nat} {v : Vector α n} {i : Nat} (h : i < n - 1) : v.pop[i] = v[i]

@[simp]

theorem Vector.getElem_pop' {α : Type u_1} {n : Nat} (v : Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) : v.pop[i] = v[i]

Variant of getElem_pop that will sometimes fire when getElem_pop gets stuck because of defeq issues in the implicit size argument.

@[simp]

theorem Vector.push_pop_back {α : Type u_1} {n : Nat} (v : Vector α (n + 1)) : push v.back v.pop = v

empty lemmas

theorem Vector.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) : map f { toArray := #[], size_toArray := ⋯ } = { toArray := #[], size_toArray := ⋯ }

theorem Vector.eq_empty {α : Type u_1} (v : Vector α 0) : v = { toArray := #[], size_toArray := ⋯ }

Decidable quantifiers.

theorem Vector.forall_zero_iff {α : Type u_1} {P : Vector α 0 → Prop} : (∀ (v : Vector α 0), P v) ↔ P { toArray := #[], size_toArray := ⋯ }

theorem Vector.forall_cons_iff {α : Type u_1} {n : Nat} {P : Vector α (n + 1) → Prop} : (∀ (v : Vector α (n + 1)), P v) ↔ ∀ (x : α) (v : Vector α n), P (push x v)

instance Vector.instDecidableForallVectorZero {α : Type u_1} (P : Vector α 0 → Prop) [Decidable (P { toArray := #[], size_toArray := ⋯ })] : Decidable (∀ (v : Vector α 0), P v)

Equations

• Vector.instDecidableForallVectorZero P = isTrue ⋯
• Vector.instDecidableForallVectorZero P = isFalse ⋯

instance Vector.instDecidableForallVectorSucc {α : Type u_1} {n : Nat} (P : Vector α (n + 1) → Prop) [Decidable (∀ (x : α) (v : Vector α n), P (push x v))] : Decidable (∀ (v : Vector α (n + 1)), P v)

Equations

• Vector.instDecidableForallVectorSucc P = decidable_of_iff' (∀ (x : α) (v : Vector α n), P (Vector.push x v)) ⋯

instance Vector.instDecidableExistsVectorZero {α : Type u_1} (P : Vector α 0 → Prop) [Decidable (P { toArray := #[], size_toArray := ⋯ })] : Decidable (∃ (v : Vector α 0), P v)

Equations

• Vector.instDecidableExistsVectorZero P = decidable_of_iff (¬∀ (v : Vector α 0), ¬P v) ⋯

instance Vector.instDecidableExistsVectorSucc {α : Type u_1} {n : Nat} (P : Vector α (n + 1) → Prop) [Decidable (∀ (x : α) (v : Vector α n), ¬P (push x v))] : Decidable (∃ (v : Vector α (n + 1)), P v)

Equations

• Vector.instDecidableExistsVectorSucc P = decidable_of_iff (¬∀ (v : Vector α (n + 1)), ¬P v) ⋯