@@ -153,7 +153,7 @@ instance DecEq a => DecEq (List a) where
153153 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
154154 decEq (x :: xs) (y :: ys) with (decEq x y)
155155 decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)
156− decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl -- maybe another yes refl
156+ decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl
157157 decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)
158158 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
159159 decEq (x :: xs) (y :: xs) | (No p) | (Yes refl) = No (\eq => lemma_x_neq_xs_eq p refl eq)
@@ -215,3 +215,12 @@ instance DecEq Float where
215215 decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
216216 else No (really_believe_me _|_)
217217
218+--------------------------------------------------------------------------------
219+-- String
220+--------------------------------------------------------------------------------
221+
222+instance DecEq String where
223+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
224+ else No (really_believe_me _|_)
225+
226+