a94fd81 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove Eq constraint from Num

commita94fd816b9b457bd1991663bcde2e76fbfba689c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 1 Mar 2012, 10:46 (15 years ago) parentf355c72

3 files changed+5−9

compare with master

unifiedsplit

idris.cabal+1−1 lib/builtins.idr+1−1 samples/interp.idr+3−7

idris.cabal+1−1

@@ -1,5 +1,5 @@

11Name: idris

2−Version: 0.9.2

2+Version: 0.9.3

33License: BSD3

44License-file: LICENSE

55Author: Edwin Brady

lib/builtins.idr+1−1

@@ -192,7 +192,7 @@ instance (Ord a, Ord b) => Ord (a, b) where

192192 else compare xr yr

193193

194194

195−class Eq a => Num a where

195+class Num a where

196196 (+) : a -> a -> a

197197 (-) : a -> a -> a

198198 (*) : a -> a -> a

samples/interp.idr+3−7

@@ -48,19 +48,15 @@ using (G : Vect Ty n)

4848 (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

4949 (==) = Op (==)

5050

51− -- Some dummy instances for Num overloading

52− instance Eq (Expr G TyInt) where

53− (==) x y = False

54−

55− instance Ord (Expr G TyInt) where

56− compare x y = EQ

51+ (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

52+ (<) = Op (<)

5753

5854 instance Num (Expr G TyInt) where

5955 (+) x y = Op (+) x y

6056 (-) x y = Op (-) x y

6157 (*) x y = Op (*) x y

6258

63− abs x = If (Op (<) x (Val 0)) (Op (-) 0 x) x

59+ abs x = IF (x < 0) THEN (-x) ELSE x

6460

6561 fromInteger = Val . fromInteger

6662