Data.TypeNat.Vect

Documentation

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

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

Constructors

VNil :: Vect a Z

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

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

A kind of fmap for Vect.

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

VCons to the end of a Vect.

vectToList :: Vect a n -> [a]

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

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

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 a l -> String

module Data.TypeNat.Nat