@[irreducible]

def Array.foldlWith' {α : Type u_1} {β : Type u_2} (xs : Array α) (f : β → (x : α) → x ∈ xs → β) (z : β) (i : ℕ) : β

Equations

• xs.foldlWith' f z i = if h : i < xs.size then xs.foldlWith' f (f z xs[i] ⋯) (i + 1) else z

def Array.foldlWith {α : Type u_1} {β : Type u_2} (xs : Array α) (f : β → (x : α) → x ∈ xs → β) (z : β) : β

Equations

• xs.foldlWith f z = xs.foldlWith' f z 0

def Array.mapWith {α : Type u_1} {β : Type u_2} (xs : Array α) (f : (x : α) → x ∈ xs → β) : Array β

Equations

• xs.mapWith f = { toList := xs.toList.mapWith fun (x : α) (h : x ∈ xs.toList) => f x ⋯ }

noncomputable def Array.dfltMapWith {α : Type u_1} {β : Type u_2} {xs : Array α} (f : (x : α) → x ∈ xs → β) (h : xs ≠ #[]) : β

Equations

• Array.dfltMapWith f_2 h_2 = ⋯.elim
• Array.dfltMapWith f_2 h_2 = ⋯.some

theorem Array.foldlWith'_cons' {α : Type u_1} {β : Type u_2} {xs : List α} {x : α} {f : β → (y : α) → y ∈ { toList := x :: xs } → β} {z : β} {i : ℕ} (h : i ≠ 0) : { toList := x :: xs }.foldlWith' f z i = { toList := xs }.foldlWith' (fun (acc : β) (x_1 : α) (h₁ : x_1 ∈ { toList := xs }) => f acc x_1 ⋯) z (i - 1)

@[simp]

theorem Array.foldlWith'_cons {α : Type u_1} {β : Type u_2} {xs : List α} {x : α} {f : β → (y : α) → y ∈ { toList := x :: xs } → β} {z : β} {i : ℕ} : { toList := x :: xs }.foldlWith' f z (i + 1) = { toList := xs }.foldlWith' (fun (acc : β) (x_1 : α) (h₁ : x_1 ∈ { toList := xs }) => f acc x_1 ⋯) z i

theorem Array.foldlWith_eq_foldlWith_toList {α : Type u_1} {β : Type u_2} {xs : Array α} {f : β → (x : α) → x ∈ xs → β} {z : β} : xs.foldlWith f z = xs.toList.foldlWith (fun (acc : β) (x : α) (h : x ∈ xs.toList) => f acc x ⋯) z

@[simp]

theorem Array.foldlWith_snoc {α : Type u_1} {β : Type u_2} {xs : Array α} {x : α} {f : β → (y : α) → y ∈ xs ++ [x] → β} {z : β} : (xs ++ [x]).foldlWith f z = f (xs.foldlWith (fun (acc : β) (y : α) (h : y ∈ xs) => f acc y ⋯) z) x ⋯

theorem Array.foldlWith_eq_foldl {α : Type u_1} {β : Type u_2} {xs : Array α} [ha : DecidableEq α] {f : β → (x : α) → x ∈ xs → β} {z : β} : xs.foldlWith f z = foldl (fun (acc : β) (x : α) => if h : x ∈ xs then f acc x h else z) z xs

theorem Array.foldlWith_eq_foldl_toList {α : Type u_1} {β : Type u_2} {xs : Array α} [ha : DecidableEq α] {f : β → (x : α) → x ∈ xs → β} {z : β} : xs.foldlWith f z = List.foldl (fun (acc : β) (x : α) => if h : x ∈ xs then f acc x h else z) z xs.toList

theorem Array.dfltMapWith_eq_dfltMapWith {α : Type u_1} {β : Type u_2} {xs : Array α} {f₁ f₂ : (x : α) → x ∈ xs → β} {h : xs ≠ #[]} : dfltMapWith f₁ h = dfltMapWith f₂ h

@[simp]

theorem Array.dfltMapWith_eq_some_of_nonempty {α : Type u_1} {β : Type u_2} {xs : Array α} [hb : Nonempty β] {f : (x : α) → x ∈ xs → β} {h : xs ≠ #[]} : dfltMapWith f h = hb.some

theorem Array.mapWith_eq_mapWith_toList {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (x : α) → x ∈ xs → β} : xs.mapWith f = { toList := xs.toList.mapWith fun (x : α) (h : x ∈ xs.toList) => f x ⋯ }

@[simp]

theorem Array.mapWith_mk {α : Type u_1} {β : Type u_2} {xs : List α} {f : (x : α) → x ∈ { toList := xs } → β} : { toList := xs }.mapWith f = { toList := xs.mapWith fun (x : α) (h : x ∈ xs) => f x ⋯ }

theorem Array.ext_iff' {α : Type u_1} {xs ys : Array α} : xs = ys ↔ xs.toList = ys.toList

theorem Array.mapWith_eq_map {α : Type u_1} {β : Type u_2} {xs : Array α} [ha : DecidableEq α] {f : (x : α) → x ∈ xs → β} : xs.mapWith f = if h : xs = #[] then #[] else map (fun (x : α) => if h₁ : x ∈ xs then f x h₁ else dfltMapWith f h) xs

theorem Array.getElem?_extract_add {α : Type u_1} {xs : Array α} {n k i : ℕ} (h : i < k) : (xs.extract n (n + k))[i]? = xs[n + i]?

theorem Array.set_eq_set! {α : Type u_1} {xs : Array α} {i : ℕ} {x : α} {h : i < xs.size} : xs.set i x h = xs.set! i x

@[simp]

theorem Array.getElem_mk {α : Type u_1} {xs : List α} {i : ℕ} {h : i < { toList := xs }.size} : { toList := xs }[i] = xs[i]