@[extern lean_array_fset]

def Array.set {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size := by get_elem_tactic) : Array α

Set an element in an array, using a proof that the index is in bounds. (This proof can usually be omitted, and will be synthesized automatically.)

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

Equations

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

@[inline]

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

Set an element in an array, or do nothing 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

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

@[reducible, inline, deprecated Array.setIfInBounds (since := "2024-11-24")]

abbrev Array.setD {α : Type u_1} (a : Array α) (i : Nat) (v : α) : Array α

Equations

• @Array.setD = @Array.setIfInBounds

@[extern lean_array_set]

def Array.set! {α : Type u_1} (a : 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

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