Documentation

data Vector a n whereSource

sLength :: Vector a n -> SNat nSource

length :: Vector a n -> IntSource

append :: Vector a n -> Vector a m -> Vector a (n :+: m)Source

foldr :: (a -> b -> b) -> b -> Vector a n -> bSource

foldl :: (a -> b -> a) -> a -> Vector b n -> aSource

singleton :: a -> Vector a (S Z)Source

zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)Source

zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c nSource

toList :: Vector a n -> [a]Source

fromList :: SNat n -> [a] -> Maybe (Vector a n)Source

unsafeFromList :: SNat n -> [a] -> Vector a nSource

fromList' :: Sing n => [a] -> Maybe (Vector a n)Source

unsafeFromList' :: Sing n => [a] -> Vector a nSource

all :: (a -> Bool) -> Vector a n -> BoolSource

splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))Source

drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)Source

take :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a nSource

map :: (a -> b) -> Vector a n -> Vector b nSource

head :: Vector a (S n) -> aSource

tail :: Vector a (S n) -> Vector a nSource