Safe Haskell | None |
---|---|
Language | Haskell2010 |
Lists of length at least 2.
Import as:
import Agda.Utils.List2 (List2(List2))
import qualified Agda.Utils.List2 as List2
Synopsis
- data List2 a = List2 a a [a]
- head :: List2 a -> a
- break :: (a -> Bool) -> List2 a -> ([a], [a])
- init :: List2 a -> List1 a
- tail :: List2 a -> List1 a
- cons :: a -> List1 a -> List2 a
- append :: List1 a -> List1 a -> List2 a
- fromList1 :: List1 a -> List2 a
- appendList :: List2 a -> [a] -> List2 a
- toList1 :: List2 a -> List1 a
- fromListMaybe :: [a] -> Maybe (List2 a)
- fromList1Maybe :: List1 a -> Maybe (List2 a)
- fromList1Either :: List1 a -> Either a (List2 a)
- toList1Either :: Either a (List2 a) -> List1 a
- toList :: IsList l => l -> [Item l]
Documentation
Lists of length ≥2.
List2 a a [a] |
Instances
Functor List2 Source # | |
Foldable List2 Source # | |
Defined in Agda.Utils.List2 fold :: Monoid m => List2 m -> m foldMap :: Monoid m => (a -> m) -> List2 a -> m foldMap' :: Monoid m => (a -> m) -> List2 a -> m foldr :: (a -> b -> b) -> b -> List2 a -> b foldr' :: (a -> b -> b) -> b -> List2 a -> b foldl :: (b -> a -> b) -> b -> List2 a -> b foldl' :: (b -> a -> b) -> b -> List2 a -> b foldr1 :: (a -> a -> a) -> List2 a -> a foldl1 :: (a -> a -> a) -> List2 a -> a elem :: Eq a => a -> List2 a -> Bool maximum :: Ord a => List2 a -> a | |
Traversable List2 Source # | |
ExprLike a => ExprLike (List2 a) Source # | |
FoldDecl a => FoldDecl (List2 a) Source # | |
Defined in Agda.Syntax.Concrete.Generic foldDecl :: Monoid m => (Declaration -> m) -> List2 a -> m Source # | |
TraverseDecl a => TraverseDecl (List2 a) Source # | |
Defined in Agda.Syntax.Concrete.Generic preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> List2 a -> m (List2 a) Source # | |
CPatternLike p => CPatternLike (List2 p) Source # | |
Defined in Agda.Syntax.Concrete.Pattern foldrCPattern :: Monoid m => (Pattern -> m -> m) -> List2 p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> List2 p -> m (List2 p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> List2 p -> m (List2 p) Source # | |
HasRange a => HasRange (List2 a) Source # | |
KillRange a => KillRange (List2 a) Source # | |
Defined in Agda.Syntax.Position killRange :: KillRangeT (List2 a) Source # | |
EmbPrj a => EmbPrj (List2 a) Source # | |
NFData a => NFData (List2 a) Source # | |
Defined in Agda.Utils.List2 | |
IsList (List2 a) Source # |
|
Show a => Show (List2 a) Source # | |
Eq a => Eq (List2 a) Source # | |
Ord a => Ord (List2 a) Source # | |
type Item (List2 a) Source # | |
Defined in Agda.Utils.List2 |
appendList :: List2 a -> [a] -> List2 a Source #
O(length first list).
fromListMaybe :: [a] -> Maybe (List2 a) Source #
Safe. O(1).
fromList1Either :: List1 a -> Either a (List2 a) Source #
toList1Either :: Either a (List2 a) -> List1 a Source #
Inverse of fromList1Either
. O(1).