git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1496 from edwinb/postulate-deceq
9701503Edwin Brady
libs/prelude/Decidable/Equality.idr+10−5
compare with master
unifiedsplit
@@ -201,7 +201,8 @@ instance DecEq a => DecEq (Vect n a) where
201
201
202instance DecEq Int where
202instance DecEq Int where
203 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
203 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
204− where postulate primitiveEq : x = y
204+ where primitiveEq : x = y
205+ primitiveEq = believe_me (refl {x})
205 postulate primitiveNotEq : x = y -> _|_
206 postulate primitiveNotEq : x = y -> _|_
206
207
207--------------------------------------------------------------------------------
208--------------------------------------------------------------------------------
@@ -210,7 +211,8 @@ instance DecEq Int where
210
211
211instance DecEq Char where
212instance DecEq Char where
212 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
213 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
213− where postulate primitiveEq : x = y
214+ where primitiveEq : x = y
215+ primitiveEq = believe_me (refl {x})
214 postulate primitiveNotEq : x = y -> _|_
216 postulate primitiveNotEq : x = y -> _|_
215
217
216--------------------------------------------------------------------------------
218--------------------------------------------------------------------------------
@@ -219,7 +221,8 @@ instance DecEq Char where
219
221
220instance DecEq Integer where
222instance DecEq Integer where
221 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
223 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
222− where postulate primitiveEq : x = y
224+ where primitiveEq : x = y
225+ primitiveEq = believe_me (refl {x})
223 postulate primitiveNotEq : x = y -> _|_
226 postulate primitiveNotEq : x = y -> _|_
224
227
225--------------------------------------------------------------------------------
228--------------------------------------------------------------------------------
@@ -228,7 +231,8 @@ instance DecEq Integer where
228
231
229instance DecEq Float where
232instance DecEq Float where
230 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
233 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
231− where postulate primitiveEq : x = y
234+ where primitiveEq : x = y
235+ primitiveEq = believe_me (refl {x})
232 postulate primitiveNotEq : x = y -> _|_
236 postulate primitiveNotEq : x = y -> _|_
233
237
234--------------------------------------------------------------------------------
238--------------------------------------------------------------------------------
@@ -237,7 +241,8 @@ instance DecEq Float where
237
241
238instance DecEq String where
242instance DecEq String where
239 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
243 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
240− where postulate primitiveEq : x = y
244+ where primitiveEq : x = y
245+ primitiveEq = believe_me (refl {x})
241 postulate primitiveNotEq : x = y -> _|_
246 postulate primitiveNotEq : x = y -> _|_
242
247
243
248