DEFINITIONS
/* This Library DEFINITION file provides a convenient access to the ProB
   external SORT function.
   This external function takes a set and translates it into a B sequence.
   It uses ProB's internal order for sorting the elements.
   It will not work for infinite sets.
   
   The SQUASH function takes a sequence with gaps and completes
   it into a proper sequence
*/
/* Include it into your machine by writing
  DEFINITIONS
      "SORT.def"
*/

 SORT(X) == [];
 EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T));
 
 SQUASH(X) == [];
 EXTERNAL_FUNCTION_SQUASH(T) == (POW(INTEGER*T)-->seq(T))
