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

Agda.Utils.List

Description

Utitlity functions on lists.

Synopsis

Documentation

mhead :: [a] -> Maybe aSource

uncons :: [a] -> Maybe (a, [a])Source

Opposite of cons `(:)`, safe.

downFrom :: Integral a => a -> [a]Source

downFrom n = [n-1,..1,0]

updateLast :: (a -> a) -> [a] -> [a]Source

Update the last element of a list, if it exists

mapEither :: (a -> Either b c) -> [a] -> ([b], [c])Source

A generalized version of `partition`. (Cf. `mapMaybe` vs. `filter`).

deal :: (a -> Either b c) -> a -> ([b], [c]) -> ([b], [c])Source

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

Sublist relation.

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.

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

Check whether a list is sorted.

Assumes that the `Ord` instance implements a partial order.

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

zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c]Source

Requires both lists to have the same length.

zipWithTails :: (a -> b -> c) -> [a] -> [b] -> ([c], [a], [b])Source

Like zipWith, but returns the leftover elements of the input lists.

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

Efficient version of nub that sorts the list first. The tag function is assumed to be cheap. If it isn't pair up the elements with their tags and call uniqBy fst (or snd).