git.iko.soy/Idris-dev
on master help sign in
Ord class
00052c8Edwin Brady
lib/builtins.idr+27−1
compare with master
unifiedsplit
@@ -111,7 +111,33 @@ instance EqInt : Eq Int;
111instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));
111instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));
112
112
113instance EqFloat : Eq Float;
113instance 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+}
115
141
116div : Int -> Int -> Int;
142div : Int -> Int -> Int;
117div = prim__divInt;
143div = prim__divInt;