Data.TypeNat.Vect

Documentation

data Vect :: Nat -> * -> * where

Nat-indexed list, where the nat determines the length.

Constructors

VNil :: Vect Z a

VCons :: a -> Vect n a -> Vect (S n) a

Instances

Functor (Vect n)

Methods

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

(<$) :: a -> Vect n b -> Vect n a

Foldable (Vect n)

Methods

fold :: Monoid m => Vect n m -> m

foldMap :: Monoid m => (a -> m) -> Vect n a -> m

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

foldr' :: (a -> b -> b) -> b -> Vect n a -> b

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

foldl' :: (b -> a -> b) -> b -> Vect n a -> b

foldr1 :: (a -> a -> a) -> Vect n a -> a

foldl1 :: (a -> a -> a) -> Vect n a -> a

toList :: Vect n a -> [a]

null :: Vect n a -> Bool

length :: Vect n a -> Int

elem :: Eq a => a -> Vect n a -> Bool

maximum :: Ord a => Vect n a -> a

minimum :: Ord a => Vect n a -> a

sum :: Num a => Vect n a -> a

product :: Num a => Vect n a -> a

Traversable (Vect n)

Methods

traverse :: Applicative f => (a -> f b) -> Vect n a -> f (Vect n b)

sequenceA :: Applicative f => Vect n (f a) -> f (Vect n a)

mapM :: Monad m => (a -> m b) -> Vect n a -> m (Vect n b)

sequence :: Monad m => Vect n (m a) -> m (Vect n a)

Eq a => Eq (Vect n a)

Methods

(==) :: Vect n a -> Vect n a -> Bool

(/=) :: Vect n a -> Vect n a -> Bool

Show a => Show (Vect n a)

Methods

showsPrec :: Int -> Vect n a -> ShowS

show :: Vect n a -> String

showList :: [Vect n a] -> ShowS

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

A kind of fmap for Vect.

vectSnoc :: a -> Vect n a -> Vect (S n) a

VCons to the end of a Vect.

vectToList :: Vect n a -> [a]

Drop the length index from a Vect, giving a typical list.

listToVect :: IsNat n => [a] -> Maybe (Vect n a)

Try to produce a Vect from a list. The nat index must be fixed somehow, perhaps with the help of ScopedTypeVariables.

showVect :: Show a => Vect l a -> String

Show a Vect.

module Data.TypeNat.Nat