@@ -254,6 +254,10 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
254concat [] = []
254concat [] = []
255concat (v::vs) = v ++ concat vs
255concat (v::vs) = v ++ concat vs
257+||| Fold without seeding the accumulator
258+foldr1 : (t -> t -> t) -> Vect (S n) t -> t
259+foldr1 f (x::xs) = foldr f x xs
257--------------------------------------------------------------------------------
261--------------------------------------------------------------------------------
259--------------------------------------------------------------------------------
263--------------------------------------------------------------------------------