diff options
Diffstat (limited to 'src/Data.hs')
| -rw-r--r-- | src/Data.hs | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Data.hs b/src/Data.hs index d83c206..1304a5f 100644 --- a/src/Data.hs +++ b/src/Data.hs @@ -139,8 +139,9 @@ vecZipWithA :: Applicative f => (a -> b -> f c) -> Vec n a -> Vec n b -> f (Vec 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 +vecInit :: Vec (S n) a -> Vec n a +vecInit (_ :< VNil) = VNil +vecInit (x :< xs@(_ :< _)) = x :< vecInit xs unsafeCoerceRefl :: a :~: b unsafeCoerceRefl = unsafeCoerce Refl |