Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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] -> BoolSource
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] -> 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.
prop_groupBy' :: (Bool -> Bool -> Bool) -> [Bool] -> PropertySource
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] -> PropertySource
tests :: IO BoolSource
Produced by Haddock version 2.6.0