no goals
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝ → α✝¹
a : α✝¹
acc : Array α✝¹
⊢ scanlTR.go f [] a acc = acc.data ++ scanl f a []
simp [scanlTR.go, scanl]
no goals
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝ → α✝¹
a✝ : α✝¹
acc : Array α✝¹
a : α✝
l : List α✝
⊢ scanlTR.go f (a :: l) a✝ acc = acc.data ++ scanl f a✝ (a :: l)
simp [scanlTR.go, scanl, scanlTR_go_eq l]