@@ -0,0 +1,46 @@
1+module Data.HVect
2+
3+using (k : Nat, ts : Vect Type k)
4+ data HVect : Vect Type k -> Type where
5+ Nil : HVect []
6+ (::) : t -> HVect ts -> HVect (t::ts)
7+
8+ index : (i : Fin k) -> HVect ts -> index i ts
9+ index fO (x::xs) = x
10+ index (fS j) (x::xs) = index j xs
11+
12+ deleteAt : {us : Vect Type (S l)} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
13+ deleteAt fO (x::xs) = xs
14+ deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
15+ deleteAt _ [] impossible
16+
17+ replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
18+ replaceAt fO y (x::xs) = y::xs
19+ replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs
20+
21+ updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
22+ updateAt fO f (x::xs) = f x :: xs
23+ updateAt (fS j) f (x::xs) = x :: updateAt j f xs
24+
25+ (++) : {us : Vect Type l} -> HVect ts -> HVect us -> HVect (ts ++ us)
26+ (++) [] ys = ys
27+ (++) (x::xs) ys = x :: (xs ++ ys)
28+
29+ instance Eq (HVect []) where
30+ [] == [] = True
31+
32+ instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
33+ (x::xs) == (y::ys) = x == y && xs == ys
34+
35+ class Shows (k : Nat) (ts : Vect Type k) where
36+ shows : HVect ts -> Vect String k
37+
38+ instance Shows O [] where
39+ shows [] = []
40+
41+ instance (Show t, Shows k ts) => Shows (S k) (t::ts) where
42+ shows (x::xs) = show x :: shows xs
43+
44+ instance (Shows k ts) => Show (HVect ts) where
45+ show xs = show (shows xs)
46+