Documentation

data Vect :: Nat -> * -> *

data SomeVect a where

nil :: Vect 0 a

cons :: a -> Vect n a -> Vect (n + 1) a

length :: Vect n a -> SNat n

head :: 1 <= n => Vect n a -> a

map :: (a -> b) -> Vect n a -> Vect n b

fromList :: [a] -> SomeVect a

toList :: Vect n a -> [a]

transpose :: Vect m (Vect n a) -> Vect n (Vect m a)

generate :: SNat n -> (Int -> a) -> Vect n a

unsafeFromList :: [a] -> Vect n a