@@ -260,10 +260,13 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
260concat [] = []
260concat [] = []
261concat (v::vs) = v ++ concat vs
261concat (v::vs) = v ++ concat vs
263−||| Fold without seeding the accumulator
263+||| Foldr without seeding the accumulator
264foldr1 : (t -> t -> t) -> Vect (S n) t -> t
264foldr1 : (t -> t -> t) -> Vect (S n) t -> t
265foldr1 f (x::xs) = foldr f x xs
265foldr1 f (x::xs) = foldr f x xs
267+||| Foldl without seeding the accumulator
268+foldl1 : (t -> t -> t) -> Vect (S n) t -> t
269+foldl1 f (x::xs) = foldl f x xs
267--------------------------------------------------------------------------------
270--------------------------------------------------------------------------------
269--------------------------------------------------------------------------------
272--------------------------------------------------------------------------------