(*
 * OK, let's see if we can define a nice library list for which IsSorted is
 * defined, which list can be used easily where appro.
 *
 * The answer is we can't do it with generics, particularly when lists are no
 * longer covariant.  Therefore, as observed elsewhere, we'll have to use
 * type variables.
 *)
obj MasterListElem;
obj MasterList =  MasterListElem*;

function IsSorted( l:MasterListElem* ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i] < l[j];

obj SomeList =  SomeElem*;
obj SomeElem < MasterListElem;

op f(l:SomeList)->boolean = (
    IsSorted(l);
);

function IsSortedV2( l:MasterList ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i] < l[j];

obj SomeListV2 < MasterList
    where: MasterListElem = SomeElemV2;
end SomeListV2;
obj SomeElemV2;

op fV2(l:SomeListV2)->boolean = (
    IsSortedV2(l);
);

obj SomeListV3 =  SomeElemV3*;
obj SomeElemV3 < MasterListElem;

op fV3(l:SomeListV3)->boolean = (
    IsSorted(l);
    IsSortedV2(l);			-- ERROR: no more list covariance
);