git.iko.soy/Idris-dev
on master help sign in
foldl1 implementation
f178bbeHeather
libs/prelude/Prelude/Strings.idr+5−1
compare with master
unifiedsplit
@@ -218,9 +218,13 @@ lines s = map pack $ lines' $ unpack s
218
218
219partial
219partial
220foldr1 : (a -> a -> a) -> List a -> a
220foldr1 : (a -> a -> a) -> List a -> a
221−foldr1 f [x] = x
221+foldr1 _ [x] = x
222foldr1 f (x::xs) = f x (foldr1 f xs)
222foldr1 f (x::xs) = f x (foldr1 f xs)
223
223
224+partial
225+foldl1 : (a -> a -> a) -> List a -> a
226+foldl1 f (x::xs) = foldl f x xs
227+
224||| Joins the character lists by spaces into a single character list.
228||| Joins the character lists by spaces into a single character list.
225|||
229|||
226||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]
230||| 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
260concat [] = []
260concat [] = []
261concat (v::vs) = v ++ concat vs
261concat (v::vs) = v ++ concat vs
262
262
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
266
266
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--------------------------------------------------------------------------------
268-- Scans
271-- Scans
269--------------------------------------------------------------------------------
272--------------------------------------------------------------------------------