SizedList
Synopsis
data SizedList n a where
 Nil :: SizedList Z a ::: :: a -> SizedList n a -> SizedList (S n) a
foldr :: forall a b n. (a -> b -> b) -> b -> SizedList n a -> b
foldrN :: forall a b n. (forall m. a -> b m -> b (S m)) -> b Z -> SizedList n a -> b n
toList :: SizedList n a -> [a]
length :: SizedList n a -> N n
fromList :: forall a n. Nat n => [a] -> Maybe (SizedList n a)
unsafeFromList :: forall a n. Nat n => [a] -> SizedList n a
replicate :: forall a n. Nat n => a -> SizedList n a
Documentation
 data SizedList n a where Source
A list which is indexed with a type-level natural that denotes the size of the list.
Constructors
 Nil :: SizedList Z a ::: :: a -> SizedList n a -> SizedList (S n) a
Instances
 Functor (SizedList n) Show a => Show (SizedList n a)
 foldr :: forall a b n. (a -> b -> b) -> b -> SizedList n a -> b Source
Fold a binary operator over a SizedList.
 foldrN :: forall a b n. (forall m. a -> b m -> b (S m)) -> b Z -> SizedList n a -> b n Source
Fold a binary operator yielding a value with a natural number indexed type over a SizedList.
 toList :: SizedList n a -> [a] Source
Convert a SizedList to a normal list.
 length :: SizedList n a -> N n Source
Returns the length of the SizedList.
 fromList :: forall a n. Nat n => [a] -> Maybe (SizedList n a) Source
Convert a normal list to a SizedList. If the length of the given list does not equal n, Nothing is returned.
 unsafeFromList :: forall a n. Nat n => [a] -> SizedList n a Source
Convert a normal list to a SizeList. If the length of the given list does not equal n, an error is thrown.
 replicate :: forall a n. Nat n => a -> SizedList n a Source
replicate x :: SizedList n a returns a SizedList of n xs.
Produced by Haddock version 2.4.2