@@ -341,13 +341,15 @@ reverse = reverse' []
342||| Insert some separator between the elements of a list.
342||| Insert some separator between the elements of a list.
344−||| > intersperse ',' (unpack "abcde") == unpack "a,b,c,d,e"
344+||| ````idris example
345+||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
346intersperse : a -> List a -> List a
348intersperse : a -> List a -> List a
347intersperse sep [] = []
349intersperse sep [] = []
348intersperse sep (x::xs) = x :: intersperse' sep xs
350intersperse sep (x::xs) = x :: intersperse' sep xs
350−-- intersperse' : a -> List a -> List a
352+ intersperse' : a -> List a -> List a
351 intersperse' sep [] = []
353 intersperse' sep [] = []
352 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
354 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
@@ -356,13 +358,15 @@ intercalate sep l = concat $ intersperse sep l
357||| Transposes rows and columns of a list of lists.
359||| Transposes rows and columns of a list of lists.
359−||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
362+||| with List transpose [[1, 2], [3, 4]]
361||| This also works for non square scenarios, thus
365||| This also works for non square scenarios, thus
362||| involution does not always hold:
366||| involution does not always hold:
364−||| > transpose [[], [1, 2]] = [[1], [2]]
368+||| transpose [[], [1, 2]] = [[1], [2]]
365−||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
369+||| transpose (transpose [[], [1, 2]]) = [[1, 2]]
367||| TODO: Solution which satisfies the totality checker?
371||| TODO: Solution which satisfies the totality checker?
368%assert_total
372%assert_total
@@ -473,7 +477,9 @@ elemIndices = elemIndicesBy (==)
474||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,
478||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,
480+||| ````idris example
476−||| > filter (<3) [0..5] == [0,1,2]
481+||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]
478filter : (a -> Bool) -> List a -> List a
484filter : (a -> Bool) -> List a -> List a
479filter p [] = []
485filter p [] = []
@@ -495,10 +501,14 @@ nubBy = nubBy' []
496 x :: nubBy' (x::acc) p xs
502 x :: nubBy' (x::acc) p xs
504+||| O(n^2). The nub function removes duplicate elements from a list. In
498−||| O(n^2). The nub function removes duplicate elements from a list. In particular, it keeps only the first occurrence of each element. It is a special case of nubBy, which allows the programmer to supply their own equality test.
505+||| particular, it keeps only the first occurrence of each element. It is a
499−|||
506+||| special case of nubBy, which allows the programmer to supply their own
500−||| > nub (the (List _) [1,2,1,3]) == [1,2,3]
507+||| equality test.
510+||| nub (the (List _) [1,2,1,3])
502nub : Eq a => List a -> List a
512nub : Eq a => List a -> List a
503nub = nubBy (==)
513nub = nubBy (==)
@@ -507,18 +517,25 @@ deleteBy : (a -> a -> Bool) -> a -> List a -> List a
507deleteBy _ _ [] = []
517deleteBy _ _ [] = []
508deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
518deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
510−||| delete x removes the first occurrence of x from its list argument. For example,
520+||| `delete x` removes the first occurrence of `x` from its list argument. For
512−||| > delete 'a' (unpack "banana") == unpack "bnana"
523+|||````idris example
524+|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']
514−||| It is a special case of deleteBy, which allows the programmer to supply their own equality test.
527+||| It is a special case of deleteBy, which allows the programmer to supply
528+||| their own equality test.
515delete : (Eq a) => a -> List a -> List a
529delete : (Eq a) => a -> List a -> List a
516delete = deleteBy (==)
530delete = deleteBy (==)
518−||| The \\ function is list difference (non-associative). In the result of xs \\ ys, the first occurrence of each element of ys in turn (if any) has been removed from xs, e.g.,
532+||| The `\\` function is list difference (non-associative). In the result of
519−|||
533+||| `xs \\ ys`, the first occurrence of each element of ys in turn (if any) has
520−||| > (([1,2] ++ [2,3]) \\ [1,2]) == [2,3]
534+||| been removed from `xs`, e.g.,
537+||| (([1,2] ++ [2,3]) \\ [1,2])
522(\\) : (Eq a) => List a -> List a -> List a
539(\\) : (Eq a) => List a -> List a -> List a
523(\\) = foldl (flip delete)
540(\\) = foldl (flip delete)
@@ -527,7 +544,9 @@ unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
528||| The union function returns the list union of the two lists. For example,
545||| The union function returns the list union of the two lists. For example,
530−||| > union (unpack "dog") (unpack "cow") == unpack "dogcw"
547+||| ```idris example
548+||| union ['d', 'o', 'g'] ['c', 'o', 'w']
532union : (Eq a) => List a -> List a -> List a
551union : (Eq a) => List a -> List a -> List a
533union = unionBy (==)
552union = unionBy (==)
@@ -539,8 +558,9 @@ union = unionBy (==)
539||| Given a list and a predicate, returns a pair consisting of the longest
558||| Given a list and a predicate, returns a pair consisting of the longest
540||| prefix of the list that satisfies a predicate and the rest of the list.
559||| prefix of the list that satisfies a predicate and the rest of the list.
542−||| > span (<3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])
562+||| span (<3) [1,2,3,2,1]
544span : (a -> Bool) -> List a -> (List a, List a)
564span : (a -> Bool) -> List a -> (List a, List a)
545span p [] = ([], [])
565span p [] = ([], [])
546span p (x::xs) =
566span p (x::xs) =
@@ -551,17 +571,20 @@ span p (x::xs) =
551 ([], x::xs)
571 ([], x::xs)
553||| Given a list and a predicate, returns a pair consisting of the longest
573||| Given a list and a predicate, returns a pair consisting of the longest
554−||| prefix of the list that does not satisfy a predicate and the rest of the list.
574+||| prefix of the list that does not satisfy a predicate and the rest of the
556−||| > break (>=3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])
578+||| break (>=3) [1,2,3,2,1]
558break : (a -> Bool) -> List a -> (List a, List a)
580break : (a -> Bool) -> List a -> (List a, List a)
559break p = span (not . p)
581break p = span (not . p)
561||| Split on any elements that satisfy the given predicate.
583||| Split on any elements that satisfy the given predicate.
563−||| > split (<2) [2,0,3,1,4] == [[2], [3], [4]]
586+||| split (<2) [2,0,3,1,4]
565split : (a -> Bool) -> List a -> List (List a)
588split : (a -> Bool) -> List a -> List (List a)
566split p xs =
589split p xs =
567 case break p xs of
590 case break p xs of
@@ -578,8 +601,9 @@ splitAt n xs = (take n xs, drop n xs)
579||| The partition function takes a predicate a list and returns the pair of lists of elements which do and do not satisfy the predicate, respectively; e.g.,
602||| The partition function takes a predicate a list and returns the pair of lists of elements which do and do not satisfy the predicate, respectively; e.g.,
581−||| > partition (<3) [0..5] == (the (List Integer) [0,1,2], the (List Integer) [3,4,5])
605+||| partition (<3) [0, 1, 2, 3, 4, 5]
583partition : (a -> Bool) -> List a -> (List a, List a)
607partition : (a -> Bool) -> List a -> (List a, List a)
584partition p [] = ([], [])
608partition p [] = ([], [])
585partition p (x::xs) =
609partition p (x::xs) =
@@ -589,19 +613,23 @@ partition p (x::xs) =
590 (lefts, x::rights)
614 (lefts, x::rights)
592−||| The inits function returns all initial segments of the argument, shortest first. For example,
616+||| The inits function returns all initial segments of the argument, shortest
593−|||
617+||| first. For example,
594−||| > inits [1,2,3] == [[],[1],[1,2],[1,2,3]]
596inits : List a -> List (List a)
622inits : List a -> List (List a)
597inits xs = [] :: case xs of
623inits xs = [] :: case xs of
599 x :: xs' => map (x ::) (inits xs')
625 x :: xs' => map (x ::) (inits xs')
601−||| The tails function returns all final segments of the argument, longest first. For example,
627+||| The tails function returns all final segments of the argument, longest
602−|||
628+||| first. For example,
603−||| > tails [1,2,3] == [[1,2,3], [2,3], [3], []]
631+||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]
605tails : List a -> List (List a)
633tails : List a -> List (List a)
606tails xs = xs :: case xs of
634tails xs = xs :: case xs of
@@ -609,14 +637,18 @@ tails xs = xs :: case xs of
610||| Split on the given element.
638||| Split on the given element.
612−||| > splitOn 0 [1,0,2,0,0,3] == [[1],[2],[],[3]]
641+||| splitOn 0 [1,0,2,0,0,3]
614splitOn : Eq a => a -> List a -> List (List a)
644splitOn : Eq a => a -> List a -> List (List a)
615splitOn a = split (== a)
645splitOn a = split (== a)
617||| Replaces all occurences of the first argument with the second argument in a list.
647||| Replaces all occurences of the first argument with the second argument in a list.
619−||| > replaceOn '-' ',' (unpack "1-2-3") == unpack "1,2,3"
650+||| replaceOn '-' ',' ['1', '-', '2', '-', '3']
621replaceOn : Eq a => a -> a -> List a -> List a
653replaceOn : Eq a => a -> a -> List a -> List a
622replaceOn a b l = map (\c => if c == a then b else c) l
654replaceOn a b l = map (\c => if c == a then b else c) l
@@ -647,8 +679,12 @@ isSuffixOf = isSuffixOfBy (==)
648||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.
680||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.
650−||| > isInfixOf "Idris" "I really like Idris." == True
682+||| ```idris example
651−||| > isInfixOf "Ial" "I really like Idris." == False
683+||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
686+||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']
653isInfixOf : Eq a => List a -> List a -> Bool
689isInfixOf : Eq a => List a -> List a -> Bool
654isInfixOf n h = any (isPrefixOf n) (tails h)
690isInfixOf n h = any (isPrefixOf n) (tails h)