Init.Data.Array.Set

Array.setIfInBounds definition

(xs : Array α) (i : Nat) (v : α) : Array α

Full source

/--
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"]`
-/
@[inline] def Array.setIfInBounds (xs : Array α) (i : Nat) (v : α) : Array α :=
  dite (LT.lt i xs.size) (fun h => xs.set i v h) (fun _ => xs)

Conditional array element replacement

Informal description

Given an array `xs` of type `α`, an index `i` of type `ℕ`, and a value `v` of type `α`, the function `setIfInBounds` returns a new array where the element at index `i` is replaced with `v` if `i` is within the bounds of the array (i.e., `i < xs.size`). If `i` is out of bounds, the original array `xs` is returned unchanged.

Array.setD abbrev

Full source

@[deprecated Array.setIfInBounds (since := "2024-11-24")] abbrev Array.setD := @Array.setIfInBounds

Default Array Element Replacement

Informal description

Given an array `xs` of type `α`, an index `i` of type `ℕ`, and a value `v` of type `α`, the function `setD` returns a new array where the element at index `i` is replaced with `v` if `i` is within the bounds of the array (i.e., `i < xs.size`). If `i` is out of bounds, the original array `xs` is returned unchanged.

Array.set! definition

(xs : Array α) (i : @& Nat) (v : α) : Array α

Full source

/--
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.
-/
@[extern "lean_array_set"]
def Array.set! (xs : Array α) (i : @& Nat) (v : α) : Array α :=
  Array.setIfInBounds xs i v

Destructive array element update (with bounds check)

Informal description

Given an array `xs` of type `α`, an index `i` of type `ℕ`, and a value `v` of type `α`, the function `Array.set!` destructively updates the array by replacing the element at index `i` with `v` if `i` is within bounds (i.e., `i < xs.size`). If `i` is out of bounds, the function panics.