@@ -166,13 +166,9 @@ total
166166vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
167167vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl
168168
169−total
170−vectDecEq : DecEq a => (x1 : Vect n a) -> (x2 : Vect n a) -> Dec (x1 = x2)
171−vectDecEq [] [] = Yes refl
172−vectDecEq (x :: xs) (y :: ys) with (decEq x y, vectDecEq xs ys)
173− vectDecEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
174− vectDecEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
175− vectDecEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
176−
177169instance DecEq a => DecEq (Vect n a) where
178− decEq = vectDecEq
170+ decEq [] [] = Yes refl
171+ decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
172+ decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
173+ decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
174+ decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))