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