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

• #[0, 1, 2].set 1 5 = #[0, 5, 2]
• #["orange", "apple"].set 1 "grape" = #["orange", "grape"]

Equations

• xs.set i v h = { toList := xs.toList.set i v }

@[inline]

def Array.setIfInBounds {α : Type u_1} (xs : Array α) (i : Nat) (v : α) : Array α

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"]

Equations

• xs.setIfInBounds i v = if h : i < xs.size then xs.set i v h else xs

@[extern lean_array_set]

def Array.set! {α : Type u_1} (xs : Array α) (i : Nat) (v : α) : Array α

Set an element in an array, or panic if the index is out of bounds.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

• xs.set! i v = xs.setIfInBounds i v