| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Utils.List1
Description
Non-empty lists.
Better name List1 for non-empty lists, plus missing functionality.
Import: @
{-# LANGUAGE PatternSynonyms #-}
import Agda.Utils.List1 (List1, pattern (:|)) import qualified Agda.Utils.List1 as List1
@
Synopsis
- type List1 = NonEmpty
- initLast :: List1 a -> ([a], a)
- snoc :: [a] -> a -> List1 a
- groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
- breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a])
- concat :: [List1 a] -> [a]
- union :: Eq a => List1 a -> List1 a -> List1 a
- ifNull :: [a] -> b -> (List1 a -> b) -> b
- ifNotNull :: [a] -> (List1 a -> b) -> b -> b
- unlessNull :: Null m => [a] -> (List1 a -> m) -> m
- allEqual :: Eq a => List1 a -> Bool
- catMaybes :: List1 (Maybe a) -> [a]
- mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
- partitionEithers :: List1 (Either a b) -> ([a], [b])
- lefts :: List1 (Either a b) -> [a]
- rights :: List1 (Either a b) -> [b]
- nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
- zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
- zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m ()
- pattern (:|) :: a -> [a] -> NonEmpty a
- zipWith :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c
- zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
- xor :: NonEmpty Bool -> Bool
- unzip :: Functor f => f (a, b) -> (f a, f b)
- unfoldr :: (a -> (b, Maybe a)) -> a -> NonEmpty b
- unfold :: (a -> (b, Maybe a)) -> a -> NonEmpty b
- uncons :: NonEmpty a -> (a, Maybe (NonEmpty a))
- transpose :: NonEmpty (NonEmpty a) -> NonEmpty (NonEmpty a)
- toList :: NonEmpty a -> [a]
- takeWhile :: (a -> Bool) -> NonEmpty a -> [a]
- take :: Int -> NonEmpty a -> [a]
- tails :: Foldable f => f a -> NonEmpty [a]
- tail :: NonEmpty a -> [a]
- splitAt :: Int -> NonEmpty a -> ([a], [a])
- span :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- sortWith :: Ord o => (a -> o) -> NonEmpty a -> NonEmpty a
- sortBy :: (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
- sort :: Ord a => NonEmpty a -> NonEmpty a
- some1 :: Alternative f => f a -> f (NonEmpty a)
- singleton :: a -> NonEmpty a
- scanr1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a
- scanr :: Foldable f => (a -> b -> b) -> b -> f a -> NonEmpty b
- scanl1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a
- scanl :: Foldable f => (b -> a -> b) -> b -> f a -> NonEmpty b
- reverse :: NonEmpty a -> NonEmpty a
- repeat :: a -> NonEmpty a
- prependList :: [a] -> NonEmpty a -> NonEmpty a
- partition :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- nubBy :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty a
- nub :: Eq a => NonEmpty a -> NonEmpty a
- nonEmpty :: [a] -> Maybe (NonEmpty a)
- map :: (a -> b) -> NonEmpty a -> NonEmpty b
- length :: NonEmpty a -> Int
- last :: NonEmpty a -> a
- iterate :: (a -> a) -> a -> NonEmpty a
- isPrefixOf :: Eq a => [a] -> NonEmpty a -> Bool
- intersperse :: a -> NonEmpty a -> NonEmpty a
- insert :: (Foldable f, Ord a) => a -> f a -> NonEmpty a
- inits :: Foldable f => f a -> NonEmpty [a]
- init :: NonEmpty a -> [a]
- head :: NonEmpty a -> a
- groupWith1 :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupWith :: (Foldable f, Eq b) => (a -> b) -> f a -> [NonEmpty a]
- groupBy1 :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupBy :: Foldable f => (a -> a -> Bool) -> f a -> [NonEmpty a]
- groupAllWith1 :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupAllWith :: Ord b => (a -> b) -> [a] -> [NonEmpty a]
- group1 :: Eq a => NonEmpty a -> NonEmpty (NonEmpty a)
- group :: (Foldable f, Eq a) => f a -> [NonEmpty a]
- fromList :: [a] -> NonEmpty a
- filter :: (a -> Bool) -> NonEmpty a -> [a]
- dropWhile :: (a -> Bool) -> NonEmpty a -> [a]
- drop :: Int -> NonEmpty a -> [a]
- cycle :: NonEmpty a -> NonEmpty a
- cons :: a -> NonEmpty a -> NonEmpty a
- break :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- appendList :: NonEmpty a -> [a] -> NonEmpty a
- append :: NonEmpty a -> NonEmpty a -> NonEmpty a
- (<|) :: a -> NonEmpty a -> NonEmpty a
- (!!) :: NonEmpty a -> Int -> a
Documentation
breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a]) Source #
Breaks a list just after an element satisfying the predicate is found.
>>>breakAfter even [1,3,5,2,4,7,8]([1,3,5,2],[4,7,8])
union :: Eq a => List1 a -> List1 a -> List1 a Source #
Like union. Duplicates in the first list are not removed.
O(nm).
unlessNull :: Null m => [a] -> (List1 a -> m) -> m Source #
allEqual :: Eq a => List1 a -> Bool Source #
Checks if all the elements in the list are equal. Assumes that
the Eq instance stands for an equivalence relation.
O(n).
partitionEithers :: List1 (Either a b) -> ([a], [b]) Source #
Like partitionEithers.
nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a) Source #
Non-efficient, monadic nub.
O(n²).
zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c) Source #
Like zipWithM.
zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b) #
The zip function takes two streams and returns a stream of
corresponding pairs.
uncons :: NonEmpty a -> (a, Maybe (NonEmpty a)) #
uncons produces the first element of the stream, and a stream of the
remaining elements, if any.
takeWhile :: (a -> Bool) -> NonEmpty a -> [a] #
returns the longest prefix of the stream
takeWhile p xsxs for which the predicate p holds.
tails :: Foldable f => f a -> NonEmpty [a] #
The tails function takes a stream xs and returns all the
suffixes of xs.
splitAt :: Int -> NonEmpty a -> ([a], [a]) #
returns a pair consisting of the prefix of splitAt n xsxs
of length n and the remaining stream immediately following this prefix.
'splitAt' n xs == ('take' n xs, 'drop' n xs)
xs == ys ++ zs where (ys, zs) = 'splitAt' n xsspan :: (a -> Bool) -> NonEmpty a -> ([a], [a]) #
returns the longest prefix of span p xsxs that satisfies
p, together with the remainder of the stream.
'span' p xs == ('takeWhile' p xs, 'dropWhile' p xs)
xs == ys ++ zs where (ys, zs) = 'span' p xssome1 :: Alternative f => f a -> f (NonEmpty a) #
sequences some1 xx one or more times.
prependList :: [a] -> NonEmpty a -> NonEmpty a #
Attach a list at the beginning of a NonEmpty.
>>>prependList [] (1 :| [2,3])1 :| [2,3]
>>>prependList [negate 1, 0] (1 :| [2, 3])-1 :| [0,1,2,3]
Since: base-4.16
partition :: (a -> Bool) -> NonEmpty a -> ([a], [a]) #
The partition function takes a predicate p and a stream
xs, and returns a pair of lists. The first list corresponds to the
elements of xs for which p holds; the second corresponds to the
elements of xs for which p does not hold.
'partition' p xs = ('filter' p xs, 'filter' (not . p) xs)iterate :: (a -> a) -> a -> NonEmpty a #
produces the infinite sequence
of repeated applications of iterate f xf to x.
iterate f x = x :| [f x, f (f x), ..]
isPrefixOf :: Eq a => [a] -> NonEmpty a -> Bool #
The isPrefixOf function returns True if the first argument is
a prefix of the second.
intersperse :: a -> NonEmpty a -> NonEmpty a #
'intersperse x xs' alternates elements of the list with copies of x.
intersperse 0 (1 :| [2,3]) == 1 :| [0,2,0,3]
insert :: (Foldable f, Ord a) => a -> f a -> NonEmpty a #
inserts insert x xsx into the last position in xs where it
is still less than or equal to the next element. In particular, if the
list is sorted beforehand, the result will also be sorted.
inits :: Foldable f => f a -> NonEmpty [a] #
The inits function takes a stream xs and returns all the
finite prefixes of xs.
groupWith1 :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) #
groupWith1 is to group1 as groupWith is to group
groupAllWith1 :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) #
groupAllWith1 is to groupWith1 as groupAllWith is to groupWith
groupAllWith :: Ord b => (a -> b) -> [a] -> [NonEmpty a] #
groupAllWith operates like groupWith, but sorts the list
first so that each equivalence class has, at most, one list in the
output
group :: (Foldable f, Eq a) => f a -> [NonEmpty a] #
The group function takes a stream and returns a list of
streams such that flattening the resulting list is equal to the
argument. Moreover, each stream in the resulting list
contains only equal elements. For example, in list notation:
'group' $ 'cycle' "Mississippi" = "M" : "i" : "ss" : "i" : "ss" : "i" : "pp" : "i" : "M" : "i" : ...
fromList :: [a] -> NonEmpty a #
Converts a normal list to a NonEmpty stream.
Raises an error if given an empty list.
filter :: (a -> Bool) -> NonEmpty a -> [a] #
removes any elements from filter p xsxs that do not satisfy p.
drop :: Int -> NonEmpty a -> [a] #
drops the first drop n xsn elements off the front of
the sequence xs.
cycle :: NonEmpty a -> NonEmpty a #
returns the infinite repetition of cycle xsxs:
cycle (1 :| [2,3]) = 1 :| [2,3,1,2,3,...]
appendList :: NonEmpty a -> [a] -> NonEmpty a #
Attach a list at the end of a NonEmpty.
>>>appendList (1 :| [2,3]) []1 :| [2,3]
>>>appendList (1 :| [2,3]) [4,5]1 :| [2,3,4,5]
Since: base-4.16