obj Enum =  a:A or b:B or c:C;
  obj A;
  obj B;
  obj C;

  op CheckEnum(e:Enum)->(e':Enum)
    pre: e?.a;		(* True if current value of e is the a alternative *)
    post: e?.c;		(* True if current value of e is the c alternative *)
  end;