foldr1 uses last element to seed accumulator
commit960a6a63c574e94fbf8a3912ba940b2035c3ce97
authorJack Ek <2727556+kjekac@users.noreply.github.com>
dateMon 3 Dec 2018, 12:10 (8 years ago)
parent595cfb4
libs/base/Data/Vect.idr+2−1
@@ -315,7 +315,8 @@ concat (v::vs) = v ++ concat vs
315315
316316||| Foldr without seeding the accumulator
317317foldr1 : (t -> t -> t) -> Vect (S n) t -> t
318−foldr1 f (x::xs) = foldr f x xs
318+foldr1 f [x] = x
319+foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
319320
320321||| Foldl without seeding the accumulator
321322foldl1 : (t -> t -> t) -> Vect (S n) t -> t