(*
 * Old idea version -- that '*' by itself is a legal type spec.  This is the
 * built-in generic list idea.
 *
function IsSorted( l:* ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i].id < l[j].id;
 *
 *)

(* 
 * Another old idea version, that uses the would-be built-in type any.
 *
function IsSorted( l:any* ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i].id < l[j].id;
 *
 *)

obj SortableElem;

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

obj ListElem < SortableElem;
op f(l:ListElem*)->boolean =
    IsSorted(l);

obj SortableListElem;
obj SortableList =  SortableListElem*;

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

obj MyList < SortableList (* is elems:integer* *)
    where: SortableListElem = integer;
end MyList;

op f(l:MyList)->boolean = (
    IsSorted(l);
    l[1] = nil
    (* l.elems[1] = nil; *)
);