Added foldr1 method to Vect.idr
commit43d33b3c865dcce9c2701550cf70dce094ea9151
authorJefferson Carpenter <jeffersoncarpenter2@gmail.com>
dateMon 26 May 2014, 09:28 (12 years ago)
parent09dec50
libs/prelude/Prelude/Vect.idr+4
@@ -254,6 +254,10 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
254254concat [] = []
255255concat (v::vs) = v ++ concat vs
256256
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
260+
257261--------------------------------------------------------------------------------
258262-- Scans
259263--------------------------------------------------------------------------------