f178bbe · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

foldl1 implementation

commitf178bbe7595d01b9b8910083912e8b81d1d0e1c8 authorHeather <heather@live.ru> dateThu 5 Jun 2014, 12:12 (12 years ago) parentbaaea97

2 files changed+9−2

unifiedsplit

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--------------------------------------------------------------------------------