Safe Haskell	None
Language	Haskell2010

Data.TypeNat.Vect

Synopsis

Documentation

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

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

Constructors

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

Instances

Eq t => Eq (Vect t n)
Show t => Show (Vect t n)

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

A kind of fmap for Vect.

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

VCons to the end of a Vect.

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

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