@@ -341,13 +341,15 @@ reverse = reverse' []
341341
342342||| Insert some separator between the elements of a list.
343343|||
344−||| > intersperse ',' (unpack "abcde") == unpack "a,b,c,d,e"
344+||| ````idris example
345+||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
346+||| ````
345347|||
346348intersperse : a -> List a -> List a
347349intersperse sep [] = []
348350intersperse sep (x::xs) = x :: intersperse' sep xs
349351 where
350−-- intersperse' : a -> List a -> List a
352+ intersperse' : a -> List a -> List a
351353 intersperse' sep [] = []
352354 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
353355
@@ -356,13 +358,15 @@ intercalate sep l = concat $ intersperse sep l
356358
357359||| Transposes rows and columns of a list of lists.
358360|||
359−||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
361+||| ```idris example
362+||| with List transpose [[1, 2], [3, 4]]
363+||| ```
360364|||
361365||| This also works for non square scenarios, thus
362366||| involution does not always hold:
363367|||
364−||| > transpose [[], [1, 2]] = [[1], [2]]
365−||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
368+||| transpose [[], [1, 2]] = [[1], [2]]
369+||| transpose (transpose [[], [1, 2]]) = [[1, 2]]
366370|||
367371||| TODO: Solution which satisfies the totality checker?
368372%assert_total
@@ -473,7 +477,9 @@ elemIndices = elemIndicesBy (==)
473477
474478||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,
475479|||
476−||| > filter (<3) [0..5] == [0,1,2]
480+||| ````idris example
481+||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]
482+||| ````
477483|||
478484filter : (a -> Bool) -> List a -> List a
479485filter p [] = []
@@ -495,10 +501,14 @@ nubBy = nubBy' []
495501 else
496502 x :: nubBy' (x::acc) p xs
497503
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.
499−|||
500−||| > nub (the (List _) [1,2,1,3]) == [1,2,3]
504+||| O(n^2). The nub function removes duplicate elements from a list. In
505+||| particular, it keeps only the first occurrence of each element. It is a
506+||| special case of nubBy, which allows the programmer to supply their own
507+||| equality test.
501508|||
509+||| ```idris example
510+||| nub (the (List _) [1,2,1,3])
511+||| ```
502512nub : Eq a => List a -> List a
503513nub = nubBy (==)
504514
@@ -507,18 +517,25 @@ deleteBy : (a -> a -> Bool) -> a -> List a -> List a
507517deleteBy _ _ [] = []
508518deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
509519
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
521+||| example,
511522|||
512−||| > delete 'a' (unpack "banana") == unpack "bnana"
523+|||````idris example
524+|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']
525+|||````
513526|||
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.
515529delete : (Eq a) => a -> List a -> List a
516530delete = deleteBy (==)
517531
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.,
519−|||
520−||| > (([1,2] ++ [2,3]) \\ [1,2]) == [2,3]
532+||| The `\\` function is list difference (non-associative). In the result of
533+||| `xs \\ ys`, the first occurrence of each element of ys in turn (if any) has
534+||| been removed from `xs`, e.g.,
521535|||
536+||| ```idris example
537+||| (([1,2] ++ [2,3]) \\ [1,2])
538+||| ```
522539(\\) : (Eq a) => List a -> List a -> List a
523540(\\) = foldl (flip delete)
524541
@@ -527,7 +544,9 @@ unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
527544
528545||| The union function returns the list union of the two lists. For example,
529546|||
530−||| > union (unpack "dog") (unpack "cow") == unpack "dogcw"
547+||| ```idris example
548+||| union ['d', 'o', 'g'] ['c', 'o', 'w']
549+||| ```
531550|||
532551union : (Eq a) => List a -> List a -> List a
533552union = unionBy (==)
@@ -539,8 +558,9 @@ union = unionBy (==)
539558||| Given a list and a predicate, returns a pair consisting of the longest
540559||| prefix of the list that satisfies a predicate and the rest of the list.
541560|||
542−||| > span (<3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])
543−|||
561+||| ```idris example
562+||| span (<3) [1,2,3,2,1]
563+||| ```
544564span : (a -> Bool) -> List a -> (List a, List a)
545565span p [] = ([], [])
546566span p (x::xs) =
@@ -551,17 +571,20 @@ span p (x::xs) =
551571 ([], x::xs)
552572
553573||| 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.
555−|||
556−||| > break (>=3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])
574+||| prefix of the list that does not satisfy a predicate and the rest of the
575+||| list.
557576|||
577+||| ```idris example
578+||| break (>=3) [1,2,3,2,1]
579+||| ```
558580break : (a -> Bool) -> List a -> (List a, List a)
559581break p = span (not . p)
560582
561583||| Split on any elements that satisfy the given predicate.
562584|||
563−||| > split (<2) [2,0,3,1,4] == [[2], [3], [4]]
564−|||
585+||| ```idris example
586+||| split (<2) [2,0,3,1,4]
587+||| ```
565588split : (a -> Bool) -> List a -> List (List a)
566589split p xs =
567590 case break p xs of
@@ -578,8 +601,9 @@ splitAt n xs = (take n xs, drop n xs)
578601
579602||| 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.,
580603|||
581−||| > partition (<3) [0..5] == (the (List Integer) [0,1,2], the (List Integer) [3,4,5])
582−|||
604+||| ```idris example
605+||| partition (<3) [0, 1, 2, 3, 4, 5]
606+||| ```
583607partition : (a -> Bool) -> List a -> (List a, List a)
584608partition p [] = ([], [])
585609partition p (x::xs) =
@@ -589,19 +613,23 @@ partition p (x::xs) =
589613 else
590614 (lefts, x::rights)
591615
592−||| The inits function returns all initial segments of the argument, shortest first. For example,
593−|||
594−||| > inits [1,2,3] == [[],[1],[1,2],[1,2,3]]
616+||| The inits function returns all initial segments of the argument, shortest
617+||| first. For example,
595618|||
619+||| ```idris example
620+||| inits [1,2,3]
621+||| ```
596622inits : List a -> List (List a)
597623inits xs = [] :: case xs of
598624 [] => []
599625 x :: xs' => map (x ::) (inits xs')
600626
601−||| The tails function returns all final segments of the argument, longest first. For example,
602−|||
603−||| > tails [1,2,3] == [[1,2,3], [2,3], [3], []]
627+||| The tails function returns all final segments of the argument, longest
628+||| first. For example,
604629|||
630+||| ```idris example
631+||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]
632+|||```
605633tails : List a -> List (List a)
606634tails xs = xs :: case xs of
607635 [] => []
@@ -609,14 +637,18 @@ tails xs = xs :: case xs of
609637
610638||| Split on the given element.
611639|||
612−||| > splitOn 0 [1,0,2,0,0,3] == [[1],[2],[],[3]]
640+||| ```idris example
641+||| splitOn 0 [1,0,2,0,0,3]
642+||| ```
613643|||
614644splitOn : Eq a => a -> List a -> List (List a)
615645splitOn a = split (== a)
616646
617647||| Replaces all occurences of the first argument with the second argument in a list.
618648|||
619−||| > replaceOn '-' ',' (unpack "1-2-3") == unpack "1,2,3"
649+||| ```idris example
650+||| replaceOn '-' ',' ['1', '-', '2', '-', '3']
651+||| ```
620652|||
621653replaceOn : Eq a => a -> a -> List a -> List a
622654replaceOn a b l = map (\c => if c == a then b else c) l
@@ -647,8 +679,12 @@ isSuffixOf = isSuffixOfBy (==)
647679
648680||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.
649681|||
650−||| > isInfixOf "Idris" "I really like Idris." == True
651−||| > isInfixOf "Ial" "I really like Idris." == False
682+||| ```idris example
683+||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
684+||| ```
685+||| ```idris example
686+||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']
687+||| ```
652688|||
653689isInfixOf : Eq a => List a -> List a -> Bool
654690isInfixOf n h = any (isPrefixOf n) (tails h)