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

mk lemmas

@[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 ⋯

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

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

Alias of Vector.set_mk.

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

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

Alias of Vector.swap_mk.

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

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

Alias of Vector.swapAt_mk.

toArray lemmas

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

theorem Vector.toArray_setD {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {x : α} : (xs.setIfInBounds i x).toArray = xs.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} {xs : Vector α n} {i : Nat} {x : α} (h : i < n) : (xs.set i x h).toArray = xs.set i x ⋯

Alias of Vector.toArray_set.

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

theorem Vector.toArray_swap! {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} : (xs.swapIfInBounds i j).toArray = xs.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} {xs : Vector α n} {i j : Nat} (hi : j < n) (hj : i < n) : (xs.swap i j hj hi).toArray = xs.swap i j ⋯ ⋯

Alias of Vector.toArray_swap.

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

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

Alias of Vector.toArray_swapAt.