A set in Magma is a (usually unordered) collection of objects belonging to some common structure (called the universe of the set). There are three basic types of sets: enumerated sets, whose elements are all stored explicitly (with one exception, see below); indexed sets, which are restricted enumerated sets having a numbering on elements; and multisets, which are enumerated sets with possible repetition of elements. Enumerated sets, indexed sets and multisets are always finite.
Enumerated sets are finite, and can be specified in three basic ways (see also section 2 below): by listing all elements; by an expression involving elements of some finite structure; and by an arithmetic progression. If an arithmetic progression is specified, the elements are not calculated explicitly until a modification of the set necessitates it; in all other cases all elements of the enumerated set are stored explicitly.
For some purposes it is useful to be able to access elements of a set through an index map, which numbers the elements of the set. For that purpose Magma has indexed sets, on which a very few basic set operations are allowed (element membership testing) as well as some sequence-like operations (such as accessing the i-th term, getting the index of an element, appending and pruning).
For some purposes it is useful to construct a set with some of its members repeated. For that purpose Magma has multisets, which take into account the repetition of members. The number of times an object x occurs in a multiset S is called the multiplicity of x in S. Magma has the ^^ operator to specify a multiplicity: the expression x^^ n means the object x with multiplicity n. In the following, whenever any multiset constructor or function expects an element y, the expression x^^ n may usually be used.
The binary operators for sets do not allow mixing of the three types of sets; functions are provided for making an enumerated set out of an indexed set or a multiset (and vice versa).
The elements of enumerated sets are restricted, in the sense that either some universe must be specified upon creation, or Magma must be able to find such universe automatically. The rules for compatibility of elements and the way Magma deals with these universes are the same for sequences and sets, and are described in the previous chapter. The restrictions on indexed sets are the same as those for enumerated sets.
Certain expressions appearing in the sections below (possibly with subscripts) have a standard interpretation: