1(* ========================================================================= *) 2(* ORDERED TYPES *) 3(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Ordered = 7sig 8 9type t 10 11val compare : t * t -> order 12 13(* 14 PROVIDES 15 16 !x : t. compare (x,x) = EQUAL 17 18 !x y : t. compare (x,y) = LESS <=> compare (y,x) = GREATER 19 20 !x y : t. compare (x,y) = EQUAL ==> compare (y,x) = EQUAL 21 22 !x y z : t. compare (x,y) = EQUAL ==> compare (x,z) = compare (y,z) 23 24 !x y z : t. 25 compare (x,y) = LESS andalso compare (y,z) = LESS ==> 26 compare (x,z) = LESS 27 28 !x y z : t. 29 compare (x,y) = GREATER andalso compare (y,z) = GREATER ==> 30 compare (x,z) = GREATER 31*) 32 33end 34