@@ -158,9 +158,11 @@ implementation DecEq a => DecEq (List a) where
158158--------------------------------------------------------------------------------
159159
160160implementation DecEq Int where
161− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
161+ decEq x y = case x == y of -- Blocks if x or y not concrete
162+ True => Yes primitiveEq
163+ False => No primitiveNotEq
162164 where primitiveEq : x = y
163− primitiveEq = believe_me (Refl {x})
165+ primitiveEq = really_believe_me (Refl {x})
164166 postulate primitiveNotEq : x = y -> Void
165167
166168--------------------------------------------------------------------------------
@@ -168,9 +170,11 @@ implementation DecEq Int where
168170--------------------------------------------------------------------------------
169171
170172implementation DecEq Char where
171− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
173+ decEq x y = case x == y of -- Blocks if x or y not concrete
174+ True => Yes primitiveEq
175+ False => No primitiveNotEq
172176 where primitiveEq : x = y
173− primitiveEq = believe_me (Refl {x})
177+ primitiveEq = really_believe_me (Refl {x})
174178 postulate primitiveNotEq : x = y -> Void
175179
176180--------------------------------------------------------------------------------
@@ -178,20 +182,23 @@ implementation DecEq Char where
178182--------------------------------------------------------------------------------
179183
180184implementation DecEq Integer where
181− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
185+ decEq x y = case x == y of -- Blocks if x or y not concrete
186+ True => Yes primitiveEq
187+ False => No primitiveNotEq
182188 where primitiveEq : x = y
183189 primitiveEq = really_believe_me (Refl {x})
184190 postulate primitiveNotEq : x = y -> Void
185191
186−
187192--------------------------------------------------------------------------------
188193-- String
189194--------------------------------------------------------------------------------
190195
191196implementation DecEq String where
192− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
197+ decEq x y = case x == y of -- Blocks if x or y not concrete
198+ True => Yes primitiveEq
199+ False => No primitiveNotEq
193200 where primitiveEq : x = y
194− primitiveEq = believe_me (Refl {x})
201+ primitiveEq = really_believe_me (Refl {x})
195202 postulate primitiveNotEq : x = y -> Void
196203
197204--------------------------------------------------------------------------------
@@ -199,9 +206,11 @@ implementation DecEq String where
199206--------------------------------------------------------------------------------
200207
201208implementation DecEq Ptr where
202− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
209+ decEq x y = case x == y of -- Blocks if x or y not concrete
210+ True => Yes primitiveEq
211+ False => No primitiveNotEq
203212 where primitiveEq : x = y
204− primitiveEq = believe_me (Refl {x})
213+ primitiveEq = really_believe_me (Refl {x})
205214 postulate primitiveNotEq : x = y -> Void
206215
207216--------------------------------------------------------------------------------
@@ -209,7 +218,9 @@ implementation DecEq Ptr where
209218--------------------------------------------------------------------------------
210219
211220implementation DecEq ManagedPtr where
212− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
221+ decEq x y = case x == y of -- Blocks if x or y not concrete
222+ True => Yes primitiveEq
223+ False => No primitiveNotEq
213224 where primitiveEq : x = y
214− primitiveEq = believe_me (Refl {x})
225+ primitiveEq = really_believe_me (Refl {x})
215226 postulate primitiveNotEq : x = y -> Void