ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.List2

Lists of length at least 2.

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

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

O(length first list).

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

O(length first list).

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

valueconcat21 :: List2 (List1 a) -> List2 a

Concatenate at least 2 lists of length at least 1.

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

O(1).

valuefromList1 :: List1 a -> List2 a

Unsafe! O(1).

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

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

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

Safe. O(1).

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

Safe. O(1).

valuehead :: List2 a -> a

Safe. O(1).

valueinit :: List2 a -> List1 a

Safe. O(n).

valuesnoc :: List1 a -> a -> List2 a

O(n).

valuetail :: List2 a -> List1 a

Safe. O(1).

valuetoList1 :: List2 a -> List1 a

Safe. O(1).

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

Inverse of fromList1Either. O(1).

datadata List2 a

Lists of length ≥2.

Instances17Functor, Foldable, Traversable, IsList, Eq, Ord, …

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

methodtoList :: l -> [Item l]

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