mk lemmas #
toArray lemmas #
@[deprecated Vector.toArray_setIfInBounds (since := "2024-11-25")]
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)
:
Alias of Vector.toArray_set
.
@[deprecated Vector.toArray_swapIfInBounds (since := "2024-11-25")]
Alias of Vector.toArray_swapIfInBounds
.
@[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)
:
Alias of Vector.toArray_swapAt
.