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