Documentation

data ListN n a #

toListN :: forall n a. (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a) #

unListN :: ListN n a -> [a] #

length :: forall a n. (KnownNat n, NatWithinBound Int n) => ListN n a -> Int #

create :: forall a n. KnownNat n => (Integer -> a) -> ListN n a #

createFrom :: forall a n start. (KnownNat n, KnownNat start) => Proxy start -> (Integer -> a) -> ListN n a #

empty :: ListN 0 a #

singleton :: a -> ListN 1 a #

uncons :: CmpNat n 0 ~ GT => ListN n a -> (a, ListN (n - 1) a) #

cons :: a -> ListN n a -> ListN (n + 1) a #

map :: (a -> b) -> ListN n a -> ListN n b #

elem :: Eq a => a -> ListN n a -> Bool #

foldl :: (b -> a -> b) -> b -> ListN n a -> b #

append :: ListN n a -> ListN m a -> ListN (n + m) a #

minimum :: (Ord a, CmpNat n 0 ~ GT) => ListN n a -> a #

maximum :: (Ord a, CmpNat n 0 ~ GT) => ListN n a -> a #

head :: CmpNat n 0 ~ GT => ListN n a -> a #

tail :: CmpNat n 0 ~ GT => ListN n a -> ListN (n - 1) a #

take :: forall a m n. (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a #

drop :: forall a d m n. (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a #

zip :: ListN n a -> ListN n b -> ListN n (a, b) #

zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c) #

zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a, b, c, d) #

zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a, b, c, d, e) #

zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x #

zipWith3 :: (a -> b -> c -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n x #

zipWith4 :: (a -> b -> c -> d -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x #

zipWith5 :: (a -> b -> c -> d -> e -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n x #

replicateM :: forall n m a. (n <= 1048576, Monad m, KnownNat n) => m a -> m (ListN n a) #