10410de · Idris-dev · git.iko.soy

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

188

189instance DecEq Int where

190− decEq x y = if x == y then Yes (believe_me (x = x))

190+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

191− else No (believe_me _|_)

191+ else No (really_believe_me _|_)

192

193--------------------------------------------------------------------------------

194-- Char

195--------------------------------------------------------------------------------

196

197instance DecEq Char where

198− decEq x y = if x == y then Yes (believe_me (x = x))

198+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

199− else No (believe_me _|_)

199+ else No (really_believe_me _|_)

200

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

202-- Integer

203--------------------------------------------------------------------------------

204

205instance DecEq Integer where

206− decEq x y = if x == y then Yes (believe_me (x = x))

206+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

207− else No (believe_me _|_)

207+ else No (really_believe_me _|_)

208

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

210-- Float

211--------------------------------------------------------------------------------

212

213instance DecEq Float where

214− decEq x y = if x == y then Yes (believe_me (x = x))

214+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

215− else No (believe_me _|_)

215+ else No (really_believe_me _|_)

216