Agda-2.2.10: A dependently typed functional programming language and proof assistant



Utitlity functions on lists.



mhead :: [a] -> Maybe aSource

type Prefix a = [a]Source

type Suffix a = [a]Source

maybePrefixMatch :: Eq a => Prefix a -> [a] -> Maybe (Suffix a)Source

Check if a list has a given prefix. If so, return the list minus the prefix.

wordsBy :: (a -> Bool) -> [a] -> [[a]]Source

Split a list into sublists. Generalisation of the prelude function words.

 words xs == wordsBy isSpace xs

chop :: Int -> [a] -> [[a]]Source

Chop up a list in chunks of a given length.

holes :: [a] -> [(a, [a])]Source

All ways of removing one element from a list.

distinct :: Eq a => [a] -> BoolSource

Check whether all elements in a list are distinct from each other. Assumes that the Eq instance stands for an equivalence relation.

fastDistinct :: Ord a => [a] -> BoolSource

An optimised version of distinct.

Precondition: The list's length must fit in an Int.

allEqual :: Eq a => [a] -> BoolSource

Checks if all the elements in the list are equal. Assumes that the Eq instance stands for an equivalence relation.

groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]Source

A variant of groupBy which applies the predicate to consecutive pairs.

groupOn :: Ord b => (a -> b) -> [a] -> [[a]]Source

groupOn f = groupBy ((==) `on` f) . sortBy (compare `on` f).

extractNthElement' :: Integral i => i -> [a] -> ([a], a, [a])Source

extractNthElement n xs gives the n-th element in xs (counting from 0), plus the remaining elements (preserving order).

extractNthElement :: Integral i => i -> [a] -> (a, [a])Source

genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe iSource