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); formal sets, whose elements are stored implicitly by means of a predicate that allows for testing membership; and indexed sets, which are restricted enumerated sets having a numbering on elements. In particular, enumerated and indexed sets are always finite, and formal sets are allowed to be infinite.
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.
A formal set consists of the subset of elements of some carrier set (structure) on which a certain predicate assumes the value `true'.
The only set-theoretic operations that can be performed on formal sets are
union, intersection, difference and symmetric difference, and element
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).
The binary operators for sets do not allow mixing of the three types of sets (so one cannot take the intersection of an enumerated set and a formal set, for example), but it is easy to convert an enumerated set into a formal set -- see the section on binary operators below -- and there are functions provided for making an enumerated set out of an indexed set (and vice versa).
By the limitation on their construction formal sets can only contain elements
from one structure in Magma. The elements of enumerated sets are also
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: