7688c8d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better DecEq implementations on primitives

7688c8dEdwin Brady11 years ago

libs/prelude/Decidable/Equality.idr+23−12

compare with master

unifiedsplit

@@ -158,9 +158,11 @@ implementation DecEq a => DecEq (List a) where

158--------------------------------------------------------------------------------

159

160implementation DecEq Int where

161+ decEq x y = case x == y of -- Blocks if x or y not concrete

162+ True => Yes primitiveEq

161− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

163+ False => No primitiveNotEq

162 where primitiveEq : x = y

164 where primitiveEq : x = y

163− primitiveEq = believe_me (Refl {x})

165+ primitiveEq = really_believe_me (Refl {x})

164 postulate primitiveNotEq : x = y -> Void

166 postulate primitiveNotEq : x = y -> Void

165

167

166--------------------------------------------------------------------------------

168--------------------------------------------------------------------------------

@@ -168,9 +170,11 @@ implementation DecEq Int where

168--------------------------------------------------------------------------------

170--------------------------------------------------------------------------------

169

171

170implementation DecEq Char where

172implementation DecEq Char where

173+ decEq x y = case x == y of -- Blocks if x or y not concrete

174+ True => Yes primitiveEq

171− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

175+ False => No primitiveNotEq

172 where primitiveEq : x = y

176 where primitiveEq : x = y

173− primitiveEq = believe_me (Refl {x})

177+ primitiveEq = really_believe_me (Refl {x})

174 postulate primitiveNotEq : x = y -> Void

178 postulate primitiveNotEq : x = y -> Void

175

179

176--------------------------------------------------------------------------------

180--------------------------------------------------------------------------------

@@ -178,20 +182,23 @@ implementation DecEq Char where

178--------------------------------------------------------------------------------

182--------------------------------------------------------------------------------

179

183

180implementation DecEq Integer where

184implementation DecEq Integer where

185+ decEq x y = case x == y of -- Blocks if x or y not concrete

186+ True => Yes primitiveEq

181− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

187+ False => No primitiveNotEq

182 where primitiveEq : x = y

188 where primitiveEq : x = y

183 primitiveEq = really_believe_me (Refl {x})

189 primitiveEq = really_believe_me (Refl {x})

184 postulate primitiveNotEq : x = y -> Void

190 postulate primitiveNotEq : x = y -> Void

185

191

186−

187--------------------------------------------------------------------------------

192--------------------------------------------------------------------------------

188-- String

193-- String

189--------------------------------------------------------------------------------

194--------------------------------------------------------------------------------

190

195

191implementation DecEq String where

196implementation DecEq String where

197+ decEq x y = case x == y of -- Blocks if x or y not concrete

198+ True => Yes primitiveEq

192− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

199+ False => No primitiveNotEq

193 where primitiveEq : x = y

200 where primitiveEq : x = y

194− primitiveEq = believe_me (Refl {x})

201+ primitiveEq = really_believe_me (Refl {x})

195 postulate primitiveNotEq : x = y -> Void

202 postulate primitiveNotEq : x = y -> Void

196

203

197--------------------------------------------------------------------------------

204--------------------------------------------------------------------------------

@@ -199,9 +206,11 @@ implementation DecEq String where

199--------------------------------------------------------------------------------

206--------------------------------------------------------------------------------

200

207

201implementation DecEq Ptr where

208implementation DecEq Ptr where

209+ decEq x y = case x == y of -- Blocks if x or y not concrete

210+ True => Yes primitiveEq

202− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

211+ False => No primitiveNotEq

203 where primitiveEq : x = y

212 where primitiveEq : x = y

204− primitiveEq = believe_me (Refl {x})

213+ primitiveEq = really_believe_me (Refl {x})

205 postulate primitiveNotEq : x = y -> Void

214 postulate primitiveNotEq : x = y -> Void

206

215

207--------------------------------------------------------------------------------

216--------------------------------------------------------------------------------

@@ -209,7 +218,9 @@ implementation DecEq Ptr where

209--------------------------------------------------------------------------------

218--------------------------------------------------------------------------------

210

219

211implementation DecEq ManagedPtr where

220implementation DecEq ManagedPtr where

221+ decEq x y = case x == y of -- Blocks if x or y not concrete

222+ True => Yes primitiveEq

212− decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

223+ False => No primitiveNotEq

213 where primitiveEq : x = y

224 where primitiveEq : x = y

214− primitiveEq = believe_me (Refl {x})

225+ primitiveEq = really_believe_me (Refl {x})

215 postulate primitiveNotEq : x = y -> Void

226 postulate primitiveNotEq : x = y -> Void