1 files changed, 12 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs
index 155eeb3..d83c206 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -115,6 +115,7 @@ data Vec n t where
   VNil :: Vec Z t
   (:<) :: t -> Vec n t -> Vec (S n) t
 deriving instance Show t => Show (Vec n t)
+deriving instance Eq t => Eq (Vec n t)
 deriving instance Functor (Vec n)
 deriving instance Foldable (Vec n)
 deriving instance Traversable (Vec n)
@@ -130,6 +131,17 @@ vecGenerate = \n f -> go n f SZ
     go SZ _ _ = VNil
     go (SS n) f i = f i :< go n f (SS i)
 
+vecReplicateA :: Applicative f => SNat n -> f a -> f (Vec n a)
+vecReplicateA SZ _ = pure VNil
+vecReplicateA (SS n) gen = (:<) <$> gen <*> vecReplicateA n gen
+
+vecZipWithA :: Applicative f => (a -> b -> f c) -> Vec n a -> Vec n b -> f (Vec n c)
+vecZipWithA _ VNil VNil = pure VNil
+vecZipWithA f (x :< xs) (y :< ys) = (:<) <$> f x y <*> vecZipWithA f xs ys
+
+vecTail :: Vec (S n) a -> Vec n a
+vecTail (_ :< xs) = xs
+
 unsafeCoerceRefl :: a :~: b
 unsafeCoerceRefl = unsafeCoerce Refl