n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v✝ : Vector α n
v : Vector α 1
⊢ scanl f b (head v ::ᵥ tail v) = b ::ᵥ f b (head (head v ::ᵥ tail v)) ::ᵥ nil
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v✝ : Vector α n
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b (head v) ::ᵥ nil
rw [← cons_head_tail v]
no goals
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v✝ : Vector α n
v : Vector α 1
⊢ scanl f b (head v ::ᵥ tail v) = b ::ᵥ f b (head (head v ::ᵥ tail v)) ::ᵥ nil
simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]