| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Utils.List

Description
Utitlity functions on lists.
Synopsis

type Prefix a = [a]
type Suffix a = [a]
maybePrefixMatch :: Eq a => Prefix a -> [a] -> Maybe (Suffix a)
wordsBy :: (a -> Bool) -> [a] -> [[a]]
chop :: Int -> [a] -> [[a]]
holes :: [a] -> [(a, [a])]
distinct :: Eq a => [a] -> Bool
allEqual :: Eq a => [a] -> Bool
groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]
prop_groupBy' :: (Bool -> Bool -> Bool) -> [Bool] -> Property
groupOn :: Ord b => (a -> b) -> [a] -> [[a]]
extractNthElement :: Integral i => i -> [a] -> (a, [a])
prop_extractNthElement :: Integer -> [Integer] -> Property
tests :: IO Bool

Documentation

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] -> Bool | Source

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

allEqual :: Eq a => [a] -> Bool | Source

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.

prop_groupBy' :: (Bool -> Bool -> Bool) -> [Bool] -> Property | Source

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

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

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

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

prop_extractNthElement :: Integer -> [Integer] -> Property | Source

tests :: IO Bool | Source

Produced by Haddock version 2.4.2