@@ -1,4 +1,4 @@
1−module Data.VectType
1+module Data.VectType
22
33import Data.Fin
44
@@ -6,7 +6,7 @@ import Data.Fin
66%default total
77
88namespace Vect {
9−
9+
1010infixr 7 ::
1111
1212%elim data Vect : Nat -> Type -> Type where
@@ -531,6 +531,8 @@ instance Applicative (Vect k) where
531531
532532 fs <*> vs = zipWith apply fs vs
533533
534+||| This monad is different from the List monad, (>>=)
535+||| uses the diagonal.
534536instance Monad (Vect n) where
535537 m >>= f = diag (map f m)
536538
@@ -539,7 +541,7 @@ instance Traversable (Vect n) where
539541 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
540542
541543--------------------------------------------------------------------------------
542−-- Show
544+-- Show
543545--------------------------------------------------------------------------------
544546
545547instance Show a => Show (Vect n a) where
@@ -595,4 +597,3 @@ instance DecEq a => DecEq (Vect n a) where
595597
596598-- For the primitives, we have to cheat because we don't have access to their
597599-- internal implementations.
598−