git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1285 from Heather/master

foldl1 implementation

commitf68b4c0ee544bb991a2c56bd7a54e5433b1c8e84 authorEdwin Brady <edwin.brady@gmail.com> dateSat 7 Jun 2014, 09:41 (12 years ago) parentbaaea97f178bbe
2 files changed+9−2
compare with master
unifiedsplit
libs/prelude/Prelude/Strings.idr+5−1 libs/prelude/Prelude/Vect.idr+4−1
libs/prelude/Prelude/Strings.idr+5−1
@@ -218,9 +218,13 @@ lines s = map pack $ lines' $ unpack s
218218
219219partial
220220foldr1 : (a -> a -> a) -> List a -> a
221−foldr1 f [x] = x
221+foldr1 _ [x] = x
222222foldr1 f (x::xs) = f x (foldr1 f xs)
223223
224+partial
225+foldl1 : (a -> a -> a) -> List a -> a
226+foldl1 f (x::xs) = foldl f x xs
227+
224228||| Joins the character lists by spaces into a single character list.
225229|||
226230||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]
libs/prelude/Prelude/Vect.idr+4−1
@@ -260,10 +260,13 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
260260concat [] = []
261261concat (v::vs) = v ++ concat vs
262262
263−||| Fold without seeding the accumulator
263+||| Foldr without seeding the accumulator
264264foldr1 : (t -> t -> t) -> Vect (S n) t -> t
265265foldr1 f (x::xs) = foldr f x xs
266266
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
267270--------------------------------------------------------------------------------
268271-- Scans
269272--------------------------------------------------------------------------------