@@ -15,6 +15,15 @@ import Prelude.List
1515import Prelude.Nat
1616import Decidable.Equality
1717
18+partial
19+foldr1 : (a -> a -> a) -> List a -> a
20+foldr1 _ [x] = x
21+foldr1 f (x::xs) = f x (foldr1 f xs)
22+
23+partial
24+foldl1 : (a -> a -> a) -> List a -> a
25+foldl1 f (x::xs) = foldl f x xs
26+
1827||| Appends two strings together.
1928|||
2029||| ```idris example
@@ -247,15 +256,6 @@ lines' s = case dropWhile isNL s of
247256lines : String -> List String
248257lines s = map pack $ lines' $ unpack s
249258
250−partial
251−foldr1 : (a -> a -> a) -> List a -> a
252−foldr1 _ [x] = x
253−foldr1 f (x::xs) = f x (foldr1 f xs)
254−
255−partial
256−foldl1 : (a -> a -> a) -> List a -> a
257−foldl1 f (x::xs) = foldl f x xs
258−
259259||| Joins the character lists by spaces into a single character list.
260260|||
261261||| ```idris example
@@ -263,12 +263,11 @@ foldl1 f (x::xs) = foldl f x xs
263263||| ```
264264unwords' : List (List Char) -> List Char
265265unwords' [] = []
266−unwords' ws = assert_total (foldr1 addSpace ws)
267− where
268− addSpace : List Char -> List Char -> List Char
269− addSpace w s = w ++ (' ' :: s)
266+unwords' ws = assert_total (foldr1 addSpace ws) where
267+ addSpace : List Char -> List Char -> List Char
268+ addSpace w s = w ++ (' ' :: s)
270269
271−||| Joins the strings by spaces into a single string.
270+||| Joins the strings by spaces into a single string.
272271|||
273272||| ```idris example
274273||| unwords ["A", "BC", "D", "E"]
@@ -276,6 +275,25 @@ unwords' ws = assert_total (foldr1 addSpace ws)
276275unwords : List String -> String
277276unwords = pack . unwords' . map unpack
278277
278+||| Joins the character lists by newlines into a single character list.
279+|||
280+||| ```idris example
281+||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
282+||| ```
283+unlines' : List (List Char) -> List Char
284+unlines' [] = []
285+unlines' ls = assert_total (foldr1 addLine ls) where
286+ addLine : List Char -> List Char -> List Char
287+ addLine l s = l ++ ('\n' :: s)
288+
289+||| Joins the strings by newlines into a single string.
290+|||
291+||| ```idris example
292+||| unlines ["line", "line2", "ln3", "D"]
293+||| ```
294+unlines : List String -> String
295+unlines = pack . unlines' . map unpack
296+
279297||| Returns the length of the string.
280298|||
281299||| ```idris example