ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.List2

Lists of length at least 2.

Import as: import Agda.Utils.List2 (List2(List2)) import qualified Agda.Utils.List2 as List2

datadata List2 a

Lists of length ≥2.

Instances16Functor, Foldable, Traversable, IsList, Eq, Ord, …

Functor List2Defined in Agda-2.7.0.1 · Agda.Utils.List2
Foldable List2Defined in Agda-2.7.0.1 · Agda.Utils.List2
Traversable List2Defined in Agda-2.7.0.1 · Agda.Utils.List2
IsList (List2 a)Defined in Agda-2.7.0.1 · Agda.Utils.List2
fromList is unsafe.
Eq a => Eq (List2 a)Defined in Agda-2.7.0.1 · Agda.Utils.List2
Ord a => Ord (List2 a)Defined in Agda-2.7.0.1 · Agda.Utils.List2
Show a => Show (List2 a)Defined in Agda-2.7.0.1 · Agda.Utils.List2
NFData a => NFData (List2 a)Defined in Agda-2.7.0.1 · Agda.Utils.List2
HasRange a => HasRange (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Position
KillRange a => KillRange (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Position
ExprLike a => ExprLike (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
FoldDecl a => FoldDecl (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
TraverseDecl a => TraverseDecl (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
CPatternLike p => CPatternLike (List2 p)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pattern
EmbPrj a => EmbPrj (List2 a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Item (List2 a) = aDefined in Agda-2.7.0.1 · Agda.Utils.List2

valuehead :: List2 a -> a

Safe. O(1).

valuebreak :: (a -> Bool) -> List2 a -> ([a], [a])

valueinit :: List2 a -> List1 a

Safe. O(n).

valuetail :: List2 a -> List1 a

Safe. O(1).

valueappend :: List1 a -> List1 a -> List2 a

O(length first list).

valuecons :: a -> List1 a -> List2 a

O(1).

valueappendList :: List2 a -> [a] -> List2 a

O(length first list).

valuetoList1 :: List2 a -> List1 a

Safe. O(1).

valuefromList1 :: List1 a -> List2 a

Unsafe! O(1).

valuefromListMaybe :: [a] -> Maybe (List2 a)

Safe. O(1).

valuefromList1Maybe :: List1 a -> Maybe (List2 a)

Safe. O(1).

valuefromList1Either :: List1 a -> Either a (List2 a)

Any List1 is either a singleton or a List2. O(1).

valuetoList1Either :: Either a (List2 a) -> List1 a

Inverse of fromList1Either. O(1).

methodtoList :: l -> [Item l]

The toList function extracts a list of Item l from the structure l. It should satisfy fromList . toList = id.