@@ -547,7 +547,8 @@ elemIndices = elemIndicesBy (==)
547547-- Filters
548548--------------------------------------------------------------------------------
549549
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.,
551552|||
552553||| ````idris example
553554||| 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)
569570 filterSmaller {p = p} (x :: xs) | True = LTESucc (filterSmaller xs)
570571
571572
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.
573575nubBy : (a -> a -> Bool) -> List a -> List a
574576nubBy = nubBy' []
575577 where
@@ -680,7 +682,9 @@ split p xs =
680682splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
681683splitAt n xs = (take n xs, drop n xs)
682684
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.,
685+||| The partition function takes a predicate a list and returns the pair of
686+||| lists of elements which do and do not satisfy the predicate, respectively;
687+||| e.g.,
684688|||
685689||| ```idris example
686690||| partition (<3) [0, 1, 2, 3, 4, 5]
@@ -763,7 +767,8 @@ isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
763767isSuffixOf : Eq a => List a -> List a -> Bool
764768isSuffixOf = isSuffixOfBy (==)
765769
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.
767772|||
768773||| ```idris example
769774||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']