@@ -111,7 +111,33 @@ instance EqInt : Eq Int;
111111instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));
112112
113113instance EqFloat : Eq Float;
114−instance EqFloat = EqInstance (boolOp prim__eqFloat)(\x, y => not (x == y));
114+instance EqFloat = EqInstance (boolOp prim__eqFloat) (\x, y => not (x == y));
115+
116+data Ordering = LT | EQ | GT;
117+
118+data Ord : Set -> Set where
119+ OrdInstance : Eq a =>
120+ (compare : a -> a -> Ordering) ->
121+ Ord a;
122+
123+ compare : Ord a => a -> a -> Ordering;
124+ compare {{OrdInstance c}} = c;
125+
126+instance OrdInt : Ord Int;
127+instance OrdInt = OrdInstance cmpInt where {
128+ cmpInt : Int -> Int -> Ordering;
129+ cmpInt x y = if (x == y) then EQ else
130+ if (boolOp prim__ltInt x y) then LT else
131+ GT;
132+}
133+
134+instance OrdFloat : Ord Float;
135+instance OrdFloat = OrdInstance cmpFloat where {
136+ cmpFloat : Float -> Float -> Ordering;
137+ cmpFloat x y = if (x == y) then EQ else
138+ if (boolOp prim__ltFloat x y) then LT else
139+ GT;
140+}
115141
116142div : Int -> Int -> Int;
117143div = prim__divInt;