@@ -174,13 +174,23 @@ total
174174vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
175175vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl
176176
177+instance DecEq a => DecEq (Vect n a) where
178+ decEq [] [] = Yes refl
179+ decEq (x :: xs) (y :: ys) with (decEq x y)
180+ decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)
181+ decEq (x :: xs) (x :: xs) | Yes refl | Yes refl = Yes refl
182+ decEq (x :: xs) (x :: ys) | Yes refl | No neq = No (neq . vectInjective2)
183+ decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)
184+
185+{- The following definition is elaborated in a wrong case-tree. Examination pending.
186+
177187instance DecEq a => DecEq (Vect n a) where
178188 decEq [] [] = Yes refl
179189 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
180190 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
181191 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
182192 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
183−
193+-}
184194
185195-- For the primitives, we have to cheat because we don't have access to their
186196-- internal implementations.