git.iko.soy/Idris-dev
on master help sign in
Fix DecEq implementation on primitives
3b35e39Edwin Brady
libs/prelude/Decidable/Equality.idr+8−13
compare with master
unifiedsplit
@@ -157,7 +157,8 @@ implementation DecEq a => DecEq (List a) where
157
157
158
158
159-- For the primitives, we have to cheat because we don't have access to their
159-- For the primitives, we have to cheat because we don't have access to their
160−-- internal implementations.
160+-- internal implementations. We postulate the inequality proofs because we're
161+-- never going to have to compute anything from them.
161
162
162--------------------------------------------------------------------------------
163--------------------------------------------------------------------------------
163-- Int
164-- Int
@@ -169,8 +170,7 @@ implementation DecEq Int where
169 False => No primitiveNotEq
170 False => No primitiveNotEq
170 where primitiveEq : x = y
171 where primitiveEq : x = y
171 primitiveEq = really_believe_me (Refl {x})
172 primitiveEq = really_believe_me (Refl {x})
172− primitiveNotEq : x = y -> Void
173+ postulate primitiveNotEq : x = y -> Void
173− primitiveNotEq = really_believe_me (id {a = x = y})
174
174
175--------------------------------------------------------------------------------
175--------------------------------------------------------------------------------
176-- Char
176-- Char
@@ -182,8 +182,7 @@ implementation DecEq Char where
182 False => No primitiveNotEq
182 False => No primitiveNotEq
183 where primitiveEq : x = y
183 where primitiveEq : x = y
184 primitiveEq = really_believe_me (Refl {x})
184 primitiveEq = really_believe_me (Refl {x})
185− primitiveNotEq : x = y -> Void
185+ postulate primitiveNotEq : x = y -> Void
186− primitiveNotEq = really_believe_me (id {a = x = y})
187
186
188--------------------------------------------------------------------------------
187--------------------------------------------------------------------------------
189-- Integer
188-- Integer
@@ -195,8 +194,7 @@ implementation DecEq Integer where
195 False => No primitiveNotEq
194 False => No primitiveNotEq
196 where primitiveEq : x = y
195 where primitiveEq : x = y
197 primitiveEq = really_believe_me (Refl {x})
196 primitiveEq = really_believe_me (Refl {x})
198− primitiveNotEq : x = y -> Void
197+ postulate primitiveNotEq : x = y -> Void
199− primitiveNotEq = really_believe_me (id {a = x = y})
200
198
201--------------------------------------------------------------------------------
199--------------------------------------------------------------------------------
202-- String
200-- String
@@ -208,8 +206,7 @@ implementation DecEq String where
208 False => No primitiveNotEq
206 False => No primitiveNotEq
209 where primitiveEq : x = y
207 where primitiveEq : x = y
210 primitiveEq = really_believe_me (Refl {x})
208 primitiveEq = really_believe_me (Refl {x})
211− primitiveNotEq : x = y -> Void
209+ postulate primitiveNotEq : x = y -> Void
212− primitiveNotEq = really_believe_me (id {a = x = y})
213
210
214--------------------------------------------------------------------------------
211--------------------------------------------------------------------------------
215-- Ptr
212-- Ptr
@@ -221,8 +218,7 @@ implementation DecEq Ptr where
221 False => No primitiveNotEq
218 False => No primitiveNotEq
222 where primitiveEq : x = y
219 where primitiveEq : x = y
223 primitiveEq = really_believe_me (Refl {x})
220 primitiveEq = really_believe_me (Refl {x})
224− primitiveNotEq : x = y -> Void
221+ postulate primitiveNotEq : x = y -> Void
225− primitiveNotEq = really_believe_me (id {a = x = y})
226
222
227--------------------------------------------------------------------------------
223--------------------------------------------------------------------------------
228-- ManagedPtr
224-- ManagedPtr
@@ -234,5 +230,4 @@ implementation DecEq ManagedPtr where
234 False => No primitiveNotEq
230 False => No primitiveNotEq
235 where primitiveEq : x = y
231 where primitiveEq : x = y
236 primitiveEq = really_believe_me (Refl {x})
232 primitiveEq = really_believe_me (Refl {x})
237− primitiveNotEq : x = y -> Void
233+ postulate primitiveNotEq : x = y -> Void
238− primitiveNotEq = really_believe_me (id {a = x = y})