4204927 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use believe_me for DecEq on primitives

This way, they can compute at the REPL, which is far more useful behaviour when testing (it is about the only legitimate use for believe_me in my opinion too :)).

commit42049275f541ee1a4a72aae648785cf0c2f691f7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 28 Aug 2014, 15:11 (12 years ago) parente1462e0

1 file changed+10−5

compare with master

unifiedsplit

libs/prelude/Decidable/Equality.idr+10−5

libs/prelude/Decidable/Equality.idr+10−5

@@ -201,7 +201,8 @@ instance DecEq a => DecEq (Vect n a) where

201201

202202instance DecEq Int where

203203 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})

205206 postulate primitiveNotEq : x = y -> _|_

206207

207208--------------------------------------------------------------------------------

@@ -210,7 +211,8 @@ instance DecEq Int where

210211

211212instance DecEq Char where

212213 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})

214216 postulate primitiveNotEq : x = y -> _|_

215217

216218--------------------------------------------------------------------------------

@@ -219,7 +221,8 @@ instance DecEq Char where

219221

220222instance DecEq Integer where

221223 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})

223226 postulate primitiveNotEq : x = y -> _|_

224227

225228--------------------------------------------------------------------------------

@@ -228,7 +231,8 @@ instance DecEq Integer where

228231

229232instance DecEq Float where

230233 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})

232236 postulate primitiveNotEq : x = y -> _|_

233237

234238--------------------------------------------------------------------------------

@@ -237,7 +241,8 @@ instance DecEq Float where

237241

238242instance DecEq String where

239243 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})

241246 postulate primitiveNotEq : x = y -> _|_

242247

243248