mk lemmas #
@[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.map_mk
{α : Type u_1}
{n : Nat}
{β : Type u_2}
(a : Array α)
(h : a.size = n)
(f : α → β)
:
Vector.map f { toArray := a, size_toArray := h } = { toArray := Array.map f a, size_toArray := ⋯ }
@[simp]
theorem
Vector.push_mk
{α : Type u_1}
{n : Nat}
(a : Array α)
(h : a.size = n)
(x : α)
:
Vector.push x { toArray := a, size_toArray := h } = { toArray := a.push x, size_toArray := ⋯ }
@[deprecated Vector.set_mk]
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
.
@[deprecated Vector.swapAt_mk]
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]
toArray lemmas #
@[simp]
@[simp]
theorem
Vector.toArray_mkEmpty
{α : Type u_1}
(cap : Nat)
:
(Vector.mkEmpty cap).toArray = Array.mkEmpty cap
@[simp]
theorem
Vector.toArray_map
{α : Type u_1}
{β : Type u_2}
{n : Nat}
(f : α → β)
(a : Vector α n)
:
(Vector.map f a).toArray = Array.map f a.toArray
@[simp]
theorem
Vector.toArray_ofFn
{n : Nat}
{α : Type u_1}
(f : Fin n → α)
:
(Vector.ofFn f).toArray = Array.ofFn f
@[simp]
theorem
Vector.toArray_push
{α : Type u_1}
{n : Nat}
(a : Vector α n)
(x : α)
:
(Vector.push x a).toArray = a.push x
@[deprecated Vector.toArray_setIfInBounds]
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]
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]
@[deprecated Vector.toArray_swapIfInBounds]
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]
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
.
@[deprecated Vector.toArray_swapAt]
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
.
toList lemmas #
getElem lemmas #
@[simp]
theorem
Vector.getElem_ofFn
{α : Type u_1}
{n : Nat}
(f : Fin n → α)
(i : Nat)
(h : i < n)
:
(Vector.ofFn f)[i] = f ⟨i, h⟩
@[simp]
theorem
Vector.getElem_push_last
{α : Type u_1}
{n : Nat}
{v : Vector α n}
{x : α}
:
(Vector.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)
:
(Vector.push x v)[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))
:
Vector.push v.back v.pop = v
empty lemmas #
theorem
Vector.map_empty
{α : Type u_1}
{β : Type u_2}
(f : α → β)
:
Vector.map f { toArray := #[], size_toArray := ⋯ } = { toArray := #[], size_toArray := ⋯ }
Decidable quantifiers. #
instance
Vector.instDecidableForallVectorZero
{α : Type u_1}
(P : Vector α 0 → Prop)
[Decidable (P { toArray := #[], size_toArray := ⋯ })]
:
instance
Vector.instDecidableForallVectorSucc
{α : Type u_1}
{n : Nat}
(P : Vector α (n + 1) → Prop)
[Decidable (∀ (x : α) (v : Vector α n), P (Vector.push x 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 := ⋯ })]
:
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 (Vector.push x v))]
:
Equations
- Vector.instDecidableExistsVectorSucc P = decidable_of_iff (¬∀ (v : Vector α (n + 1)), ¬P v) ⋯