@@ -42,6 +42,24 @@ instance Eq (HVect []) where
4242instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
4343 (x::xs) == (y::ys) = x == y && xs == ys
4444
45+total
46+hvectInjective1 : {xs, ys: HVect ts} -> {x, y:a} -> x :: xs = y :: ys -> x = y
47+hvectInjective1 Refl = Refl
48+
49+total
50+hvectInjective2 : {xs, ys: HVect ts} -> {x, y:a} -> x :: xs = y :: ys -> xs = ys
51+hvectInjective2 Refl = Refl
52+
53+instance DecEq (HVect []) where
54+ decEq [] [] = Yes Refl
55+
56+instance (DecEq t, DecEq (HVect ts)) => DecEq (HVect (t::ts)) where
57+ decEq (x::xs) (y::ys) with (decEq x y)
58+ decEq (z::xs) (z::ys) | Yes Refl with (decEq xs ys)
59+ decEq (z::zs) (z::zs) | Yes Refl | Yes Refl = Yes Refl
60+ decEq (z::xs) (z::ys) | Yes Refl | No ctr = No (ctr . hvectInjective2)
61+ decEq (x::xs) (y::ys) | No ctr = No (ctr . hvectInjective1)
62+
4563class Shows (k : Nat) (ts : Vect k Type) where
4664 shows : HVect ts -> Vect k String
4765