@@ -42,6 +42,24 @@ instance Eq (HVect []) where
42instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
42instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
43 (x::xs) == (y::ys) = x == y && xs == ys
43 (x::xs) == (y::ys) = x == y && xs == ys
46+hvectInjective1 : {xs, ys: HVect ts} -> {x, y:a} -> x :: xs = y :: ys -> x = y
47+hvectInjective1 Refl = Refl
50+hvectInjective2 : {xs, ys: HVect ts} -> {x, y:a} -> x :: xs = y :: ys -> xs = ys
51+hvectInjective2 Refl = Refl
53+instance DecEq (HVect []) where
54+ decEq [] [] = Yes Refl
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)
45class Shows (k : Nat) (ts : Vect k Type) where
63class Shows (k : Nat) (ts : Vect k Type) where
46 shows : HVect ts -> Vect k String
64 shows : HVect ts -> Vect k String