@@ -547,7 +547,8 @@ elemIndices = elemIndicesBy (==)
547-- Filters
547-- Filters
548--------------------------------------------------------------------------------
548--------------------------------------------------------------------------------
550−||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,
550+||| filter, applied to a predicate and a list, returns the list of those
551+||| elements that satisfy the predicate; e.g.,
552||| ````idris example
553||| ````idris example
553||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]
554||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]
@@ -569,7 +570,8 @@ filterSmaller {p} (x :: xs) with (p x)
569 filterSmaller {p = p} (x :: xs) | True = LTESucc (filterSmaller xs)
570 filterSmaller {p = p} (x :: xs) | True = LTESucc (filterSmaller xs)
572−||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.
573+||| The nubBy function behaves just like nub, except it uses a user-supplied
574+||| equality predicate instead of the overloaded == function.
573nubBy : (a -> a -> Bool) -> List a -> List a
575nubBy : (a -> a -> Bool) -> List a -> List a
574nubBy = nubBy' []
576nubBy = nubBy' []
@@ -680,7 +682,9 @@ split p xs =
680splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
682splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
681splitAt n xs = (take n xs, drop n xs)
683splitAt n xs = (take n xs, drop n xs)
685+||| The partition function takes a predicate a list and returns the pair of
683−||| 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.,
686+||| lists of elements which do and do not satisfy the predicate, respectively;
685||| ```idris example
689||| ```idris example
686||| partition (<3) [0, 1, 2, 3, 4, 5]
690||| partition (<3) [0, 1, 2, 3, 4, 5]
@@ -763,7 +767,8 @@ isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
763isSuffixOf : Eq a => List a -> List a -> Bool
767isSuffixOf : Eq a => List a -> List a -> Bool
764isSuffixOf = isSuffixOfBy (==)
768isSuffixOf = isSuffixOfBy (==)
766−||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.
770+||| The isInfixOf function takes two lists and returns True iff the first list
771+||| is contained, wholly and intact, anywhere within the second.
768||| ```idris example
773||| ```idris example
769||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
774||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']