@@ -21,22 +21,20 @@ mult (S k) y = plus y (mult k y);
21instance numNat : Num Nat;
21instance numNat : Num Nat;
22instance numNat = instanceNum plus sub mult;
22instance numNat = instanceNum plus sub mult;
24−instance EqNat : Eq Nat;
24+instance Eq Nat where {
25−instance EqNat = instanceEq eqNat (\x, y => not (x == y)) where {
26− eqNat : Nat -> Nat -> Bool;
27− eqNat O O = True;
25+ O == O = True;
28− eqNat (S x) (S y) = eqNat x y;
26+ (S x) == (S y) = x == y;
29− eqNat O (S y) = False;
27+ O == (S y) = False;
30− eqNat (S x) O = False;
28+ (S x) == O = False;
30+ x /= y = not (x == y);
33−instance OrdNat : Ord Nat;
33+instance Ord Nat where {
34−instance OrdNat = instanceOrd cmpNat where {
34+ compare O O = EQ;
35− cmpNat : Nat -> Nat -> Ordering;
37− cmpNat O (S k) = LT;
35+ compare O (S k) = LT;
38− cmpNat (S k) O = GT;
36+ compare (S k) O = GT;
39− cmpNat (S x) (S y) = cmpNat x y;
37+ compare (S x) (S y) = compare x y;
42plusnO : (m : Nat) -> m + O = m;
40plusnO : (m : Nat) -> m + O = m;