@@ -153,7 +153,7 @@ instance DecEq a => DecEq (List a) where
153 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
153 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
154 decEq (x :: xs) (y :: ys) with (decEq x y)
154 decEq (x :: xs) (y :: ys) with (decEq x y)
155 decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)
155 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
157 decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)
157 decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)
158 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
158 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
159 decEq (x :: xs) (y :: xs) | (No p) | (Yes refl) = No (\eq => lemma_x_neq_xs_eq p refl eq)
159 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
215 decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
215 decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
216 else No (really_believe_me _|_)
216 else No (really_believe_me _|_)
218+--------------------------------------------------------------------------------
220+--------------------------------------------------------------------------------
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 _|_)