idxOf?

theorem Array.idxOf?_toList {α : Type u_1} [BEq α] {a : α} {l : Array α} : List.idxOf? a l.toList = l.idxOf? a

erase

@[simp]

theorem Array.toList_erase {α : Type u_1} [BEq α] (l : Array α) (a : α) : (l.erase a).toList = l.toList.erase a

@[simp]

theorem Array.size_eraseIdxIfInBounds {α : Type u_1} (a : Array α) (i : Nat) : (a.eraseIdxIfInBounds i).size = if i < a.size then a.size - 1 else a.size

theorem Array.toList_drop {α : Type u_1} (as : Array α) (n : Nat) : (as.drop n).toList = List.drop n as.toList

set

map

mem

insertAt

extract

@[simp]

theorem Array.extract_empty_of_start_eq_stop {α : Type u_1} {i : Nat} {a : Array α} : a.extract i i = #[]

theorem Array.extract_append_of_stop_le_size_left {α : Type u_1} {j i : Nat} {a b : Array α} (h : j ≤ a.size) : (a ++ b).extract i j = a.extract i j

theorem Array.extract_append_of_size_left_le_start {α : Type u_1} {i j : Nat} {a b : Array α} (h : a.size ≤ i) : (a ++ b).extract i j = b.extract (i - a.size) (j - a.size)

theorem Array.extract_eq_of_size_le_stop {α : Type u_1} {j i : Nat} {a : Array α} (h : a.size ≤ j) : a.extract i j = a.extract i

swapIfInBounds

@[simp]

theorem Array.toList_swapIfInBounds {α : Type u_1} {i j : Nat} {a : Array α} : (a.swapIfInBounds i j).toList = a.toList.swap i j