List.scanl and List.scanr

theorem List.length_scanl {α : Type u_1} {β : Type u_2} {f : β → α → β} (a : β) (l : List α) : (scanl f a l).length = l.length + 1

@[simp]

theorem List.scanl_nil {α : Type u_1} {β : Type u_2} {f : β → α → β} (b : β) : scanl f b [] = [b]

@[simp]

theorem List.scanl_cons {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {a : α} {l : List α} : scanl f b (a :: l) = [b] ++ scanl f (f b a) l

@[simp]

theorem List.getElem?_scanl_zero {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {l : List α} : (scanl f b l)[0]? = some b

@[simp]

theorem List.getElem_scanl_zero {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {l : List α} {h : 0 < (scanl f b l).length} : (scanl f b l)[0] = b

theorem List.get?_succ_scanl {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {l : List α} {i : ℕ} : (scanl f b l).get? (i + 1) = ((scanl f b l).get? i).bind fun (x : β) => Option.map (fun (y : α) => f x y) (l.get? i)

theorem List.getElem_succ_scanl {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {l : List α} {i : ℕ} (h : i + 1 < (scanl f b l).length) : (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]

@[deprecated List.getElem_succ_scanl (since := "2024-08-22")]

theorem List.get_succ_scanl {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {l : List α} {i : ℕ} {h : i + 1 < (scanl f b l).length} : (scanl f b l).get ⟨i + 1, h⟩ = f ((scanl f b l).get ⟨i, ⋯⟩) (l.get ⟨i, ⋯⟩)

@[simp]

theorem List.scanr_nil {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) : scanr f b [] = [b]

@[simp]

theorem List.scanr_cons {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (a : α) (l : List α) : scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l