mk lemmas #
@[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)
:
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)
:
Alias of Vector.swapAt_mk
.
toArray lemmas #
@[deprecated Vector.toArray_setIfInBounds (since := "2024-11-25")]
Alias of Vector.toArray_setIfInBounds
.
@[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}
{xs : Vector α n}
{i : Nat}
{x : α}
(h : i < n)
:
Alias of Vector.toArray_swapAt
.