git.iko.soy/Idris-dev
on master help sign in
Eq class, Nat is a Num
commitfb233c930c1fc95e5363c5e8ead24f37d60e1176 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 4 Nov 2011, 14:13 (15 years ago) parentbe3a53a
3 files changed+40−20
compare with master
unifiedsplit
lib/builtins.idr+21−6 lib/maybe.idr+4 lib/nat.idr+15−14
lib/builtins.idr+21−6
@@ -56,6 +56,10 @@ infix 4 &&, ||;
5656(&&) True x = x;
5757(&&) False _ = False;
5858
59+not : Bool -> Bool;
60+not True = False;
61+not False = True;
62+
5963infixl 5 ==, /=, ==.;
6064infixl 6 <, <=, >, >=, <., <=., >., >=.;
6165infixl 7 <<, >>;
@@ -92,12 +96,26 @@ instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;
9296instance numFloat : Num Float;
9397instance numFloat = NumInstance prim__addFloat prim__subFloat prim__mulFloat;
9498
99+data Eq : Set -> Set where
100+ EqInstance : (eq : a -> a -> Bool) ->
101+ (neq : a -> a -> Bool) ->
102+ Eq a;
103+
104+ (==) : Eq a => a -> a -> Bool;
105+ (==) {{EqInstance eq neq}} x y = eq x y;
106+
107+ (/=) : Eq a => a -> a -> Bool;
108+ (/=) {{EqInstance eq neq}} x y = neq x y;
109+
110+instance EqInt : Eq Int;
111+instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));
112+
113+instance EqFloat : Eq Float;
114+instance EqFloat = EqInstance (boolOp prim__eqFloat)(\x, y => not (x == y));
115+
95116div : Int -> Int -> Int;
96117div = prim__divInt;
97118
98−(==) : Int -> Int -> Bool;
99−(==) = boolOp prim__eqInt;
100−
101119(<) : Int -> Int -> Bool;
102120(<) = boolOp prim__ltInt;
103121
@@ -113,9 +131,6 @@ div = prim__divInt;
113131(/) : Float -> Float -> Float;
114132(/) = prim__divFloat;
115133
116−(==.) : Float -> Float -> Bool;
117−(==.) = boolOp prim__eqFloat;
118−
119134(<.) : Float -> Float -> Bool;
120135(<.) = boolOp prim__ltFloat;
121136
lib/maybe.idr+4
@@ -5,3 +5,7 @@ maybe : b -> (a -> b) -> Maybe a -> b;
55maybe n j Nothing = n;
66maybe n j (Just x) = j x;
77
8+maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b;
9+maybe_bind Nothing k = Nothing;
10+maybe_bind (Just x) k = k x;
11+
lib/nat.idr+15−14
@@ -9,15 +9,27 @@ plus (S k) y = S (plus k y);
99eqRespS : m = n -> S m = S n;
1010eqRespS refl = refl;
1111
12−plusnO : (m : Nat) -> plus m O = m;
12+sub : Nat -> Nat -> Nat;
13+sub O y = O;
14+sub (S k) (S y) = sub k y;
15+sub x O = x;
16+
17+mult : Nat -> Nat -> Nat;
18+mult O y = O;
19+mult (S k) y = plus y (mult k y);
20+
21+instance numNat : Num Nat;
22+instance numNat = NumInstance plus sub mult;
23+
24+plusnO : (m : Nat) -> m + O = m;
1325plusnO O = refl;
1426plusnO (S k) = eqRespS (plusnO k);
1527
16−plusn_Sm : (n : Nat) -> (m : Nat) -> plus n (S m) = S (plus n m);
28+plusn_Sm : (n : Nat) -> (m : Nat) -> n + S m = S (n + m);
1729plusn_Sm O m = refl;
1830plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);
1931
20−plus_commutes : (n : Nat) -> (m : Nat) -> plus n m = plus m n;
32+plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n;
2133plus_commutes O m = sym (plusnO m);
2234plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk;
2335
@@ -28,14 +40,3 @@ plus_commutes_Sk = proof {
2840 refine plusn_Sm;
2941};
3042
31−sub : Nat -> Nat -> Nat;
32−sub O y = O;
33−sub (S k) (S y) = sub k y;
34−sub x O = x;
35−
36−mult : Nat -> Nat -> Nat;
37−mult O y = O;
38−mult (S k) y = plus y (mult k y);
39−
40−instance numNat : Num Nat;
41−instance numNat = NumInstance plus sub mult;