@@ -177,3 +177,40 @@ instance DecEq a => DecEq (Vect n a) where
177 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
177 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
178 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
178 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
179 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
179 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
182+-- For the primitives, we have to cheat because we don't have access to their
183+-- internal implementations.
185+--------------------------------------------------------------------------------
187+--------------------------------------------------------------------------------
189+instance DecEq Int where
190+ decEq x y = if x == y then Yes (believe_me (x = x))
191+ else No (believe_me _|_)
193+--------------------------------------------------------------------------------
195+--------------------------------------------------------------------------------
197+instance DecEq Char where
198+ decEq x y = if x == y then Yes (believe_me (x = x))
199+ else No (believe_me _|_)
201+--------------------------------------------------------------------------------
203+--------------------------------------------------------------------------------
205+instance DecEq Integer where
206+ decEq x y = if x == y then Yes (believe_me (x = x))
207+ else No (believe_me _|_)
209+--------------------------------------------------------------------------------
211+--------------------------------------------------------------------------------
213+instance DecEq Float where
214+ decEq x y = if x == y then Yes (believe_me (x = x))
215+ else No (believe_me _|_)