diff options
author | Tom Smeding <t.j.smeding@uu.nl> | 2025-03-07 17:35:26 +0100 |
---|---|---|
committer | Tom Smeding <t.j.smeding@uu.nl> | 2025-03-07 17:35:26 +0100 |
commit | da5dbc4ebca51a32b43bec360470c037cab1755f (patch) | |
tree | c7d03ca5b28b4a23e32a937191a3883f391bb271 /src/Data.hs | |
parent | 3a738bd9c519fe890c03948eba1e1033b93a811a (diff) |
idana: Cleanup
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 |