d656534 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4091 from jdevuyst/fix-issue-4090

d656534Ahmad Salim Al-Sibahi9 years ago

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -120,6 +120,7 @@ John Connor

120John Dobronszki

121John Wiegley

122Jon Atack

123+Jonas De Vuyst

123Jonas Westerlund

124Jonas Westerlund

124Jonathan Sterling

125Jonathan Sterling

125Joomy Korkut

126Joomy Korkut

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

@@ -169,7 +169,8 @@ implementation DecEq Int where

169 False => No primitiveNotEq

170 where primitiveEq : x = y

171 primitiveEq = really_believe_me (Refl {x})

172− postulate primitiveNotEq : x = y -> Void

172+ primitiveNotEq : x = y -> Void

173+ primitiveNotEq = really_believe_me (id {a = x = y})

173

174

174--------------------------------------------------------------------------------

175--------------------------------------------------------------------------------

175-- Char

176-- Char

@@ -181,7 +182,8 @@ implementation DecEq Char where

181 False => No primitiveNotEq

182 False => No primitiveNotEq

182 where primitiveEq : x = y

183 where primitiveEq : x = y

183 primitiveEq = really_believe_me (Refl {x})

184 primitiveEq = really_believe_me (Refl {x})

184− postulate primitiveNotEq : x = y -> Void

185+ primitiveNotEq : x = y -> Void

186+ primitiveNotEq = really_believe_me (id {a = x = y})

185

187

186--------------------------------------------------------------------------------

188--------------------------------------------------------------------------------

187-- Integer

189-- Integer

@@ -193,7 +195,8 @@ implementation DecEq Integer where

193 False => No primitiveNotEq

195 False => No primitiveNotEq

194 where primitiveEq : x = y

196 where primitiveEq : x = y

195 primitiveEq = really_believe_me (Refl {x})

197 primitiveEq = really_believe_me (Refl {x})

196− postulate primitiveNotEq : x = y -> Void

198+ primitiveNotEq : x = y -> Void

199+ primitiveNotEq = really_believe_me (id {a = x = y})

197

200

198--------------------------------------------------------------------------------

201--------------------------------------------------------------------------------

199-- String

202-- String

@@ -205,7 +208,8 @@ implementation DecEq String where

205 False => No primitiveNotEq

208 False => No primitiveNotEq

206 where primitiveEq : x = y

209 where primitiveEq : x = y

207 primitiveEq = really_believe_me (Refl {x})

210 primitiveEq = really_believe_me (Refl {x})

208− postulate primitiveNotEq : x = y -> Void

211+ primitiveNotEq : x = y -> Void

212+ primitiveNotEq = really_believe_me (id {a = x = y})

209

213

210--------------------------------------------------------------------------------

214--------------------------------------------------------------------------------

211-- Ptr

215-- Ptr

@@ -217,7 +221,8 @@ implementation DecEq Ptr where

217 False => No primitiveNotEq

221 False => No primitiveNotEq

218 where primitiveEq : x = y

222 where primitiveEq : x = y

219 primitiveEq = really_believe_me (Refl {x})

223 primitiveEq = really_believe_me (Refl {x})

220− postulate primitiveNotEq : x = y -> Void

224+ primitiveNotEq : x = y -> Void

225+ primitiveNotEq = really_believe_me (id {a = x = y})

221

226

222--------------------------------------------------------------------------------

227--------------------------------------------------------------------------------

223-- ManagedPtr

228-- ManagedPtr

@@ -229,4 +234,5 @@ implementation DecEq ManagedPtr where

229 False => No primitiveNotEq

234 False => No primitiveNotEq

230 where primitiveEq : x = y

235 where primitiveEq : x = y

231 primitiveEq = really_believe_me (Refl {x})

236 primitiveEq = really_believe_me (Refl {x})

232− postulate primitiveNotEq : x = y -> Void

237+ primitiveNotEq : x = y -> Void

238+ primitiveNotEq = really_believe_me (id {a = x = y})