Safe Haskell | None |
---|---|

Language | Haskell2010 |

# Documentation

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

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

#### Instances

Functor (Vect n) Source # | |

Foldable (Vect n) Source # | |

Defined in Data.TypeNat.Vect fold :: Monoid m => Vect n m -> m # foldMap :: Monoid m => (a -> m) -> Vect n a -> 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 # elem :: Eq a => a -> Vect n a -> Bool # maximum :: Ord a => Vect n a -> a # minimum :: Ord a => Vect n a -> a # | |

Traversable (Vect n) Source # | |

Eq a => Eq (Vect n a) Source # | |

Show a => Show (Vect n a) Source # | |

vectToList :: Vect n a -> [a] Source #

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

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

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

module Data.TypeNat.Nat