MODULE TWideSet;
(* Wide set implementation limits: a large explicit span and the
   implicit SET OF CARDINAL span. *)
TYPE
  Wide = SET OF [0..100000];
  CardSet = SET OF CARDINAL;
VAR
  w : Wide;
  c : CardSet;
  ExitCode : INTEGER;
BEGIN
  w := Wide{};
  INCL(w, 100000);
  c := CardSet{};
  INCL(c, 2);
  INCL(c, 65535);
  IF (100000 IN w) AND (2 IN c) AND (65535 IN c)
     AND NOT (3 IN c) THEN
    ExitCode := 42
  ELSE
    ExitCode := 1
  END
END TWideSet.