Merge branch 'master' of github.com:idris-lang/Idris-dev
commitdb05606968fdba6bd7239d62452d814869494056
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateWed 28 May 2014, 23:28 (12 years ago)
parent5aa2a8e4bd9c2a
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--------------------------------------------------------------------------------