@[extern lean_array_fset]
def
Array.set
{α : Type u_1}
(xs : Array α)
(i : Nat)
(v : α)
(h : i < xs.size := by get_elem_tactic)
:
Array α
Replaces the element at a given index in an array.
No bounds check is performed, but the function requires a proof that the index is in bounds. This proof can usually be omitted, and will be synthesized automatically.
The array is modified in-place if there are no other references to it.
Examples:
Equations
Instances For
@[inline]
Replaces the element at the provided index in an array. The array is returned unmodified if the index is out of bounds.
The array is modified in-place if there are no other references to it.
Examples:
#[0, 1, 2].setIfInBounds 1 5 = #[0, 5, 2]
#["orange", "apple"].setIfInBounds 1 "grape" = #["orange", "grape"]
#["orange", "apple"].setIfInBounds 5 "grape" = #["orange", "apple"]