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