====== Standard Library ======

===== Modules ''Naturals'', ''Integers'', ''Reals'' =====

  * ''Nat'', ''Int'', ''Real''
  * ''+'', ''−'', ''∗'', ''/'', ''^''
  * ''<='', ''>='', ''>'', ''<''
  * ''..''
  * ''Infinity''

===== Module ''Sequences'' =====
The Sequences module defines operations on finite sequences. We represent a finite sequence as a tuple, so the sequence of three numbers 3, 2, 1 is the triple <<3, 2, 1>>. The Sequences module defines the following operators on sequences:
  * ''s \o t'': The sequence obtained by concatenating the sequences s and t. 
    * Example: ''<<3, 7>> \o <<3>>'' is equal to ''<<3, 7, 3>>''.
  * ''Head(s)'': The first element of the sequence s.
    * Example: ''Head(<<3,2,1>>)'' is equal to ''3''
  * ''SelectSeq(s, Test)'': The subsequence of s consisting of the elements s[i] such that Test(s[i]) equals true.
    * Example: <code latex>PosSubSeq(s) == LET IsPos(n) == n > 0
                in SelectSeq(s, IsPos)</code> defines ''PosSubSeq(<<0, 3, −2, 5>>)'' to be equal to ''<<3, 5>>''
  * ''SubSeq(s, m, n)'': The subsequence ''<<s[m], s[m + 1], . . . , s[n]>>'' consisting of the mth through nth elements of s. It is undefined if ''m < 1'' or ''n > Len(s)'', except that it equals the empty sequence if ''m > n''.
  * ''Append(s, e)'': The sequence obtained by appending element e to the tail of sequence s. 
    * Example: ''Append(<<3, 7>>, 3)'' equals ''<<3, 7, 3>>''.
  * ''Len(s)'': The length of sequence s. 
    * Example: ''Len(<<1,2,3>>)'' is equal to ''3''.
  * ''Seq(S)'': The set of all sequences of elements of the set S . 
    * Example: ''Seq({3,7})'' is equal to ''<<3, 7>>''.
  * ''Tail(s)'': The tail of sequence ''s'', which consists of ''s'' with its head element removed.
    * Example: ''Tail(<<3, 7>>)'' equals ''<<7>>''.

===== Module ''FiniteSets'' =====

  * ''IsFiniteSet(s)'': A set is finite iff there is a finite sequence containing all its elements.
    * Example: ''IsFiniteSet({1,2,3})'' is equal to ''TRUE''
  * ''Cardinality(s)'': The number of elements in the set s. It's only defined for finite sets.
    * Example: ''Cardinality({1,2})'' is equal to 2.

===== Module ''Bags'' =====

  * ''(+)'', ''(-)''
  * ''BagIn''
  * ''CopiesIn''
  * ''SubBag''
  * ''BagOfAll''
  * ''EmptyBag''
  * ''\sqsubseteq''
  * ''BagToSet''
  * ''IsABag''
  * ''BagCardinality''
  * ''BagUnion''
  * ''SetToBag''

===== Module ''RealTime'' =====

  * ''RTBound''
  * ''RTnow''
  * ''now''

===== Module ''TLC'' =====

  * '':>'', ''@@''
  * ''Print'' 
  * ''Assert''
  * ''JavaTime''
  * ''Permutations''
  * ''SortSeq''