Square brackets are used for the definition of enumerated sequences; formal sequences are delimited by the composite brackets [! and !].
Certain expressions appearing below (possibly with subscripts) have the standard interpretation:
The formal sequence constructor has the following fixed format (the expressions appearing in the construct are defined above):
Create the formal sequence consisting of the subsequence of elements x of F for which P(x) is true. If P(x) is true for every element of F, the sequence constructor may be abbreviated to [! x in F !]
Sequences can be constructed by expressions enclosed in square brackets, provided that the values of all expressions can be automatically coerced into some common structure, as outlined in the Introduction. All general constructors have the universe U optionally up front, which allows the user to specify into which structure all terms of the sequences should be coerced.
The null sequence (empty, and no universe specified).
The empty sequence with universe U.
Given a list of expressions e1, ..., en, defining elements a1, a2, ..., an all belonging to (or automatically coercible into) a single algebraic structure U, create the sequence Q = [ a1, a2, ..., an ] of elements of U.As for multisets, one may use the expression x^^ n to specify the object x with multiplicity n: this is simply interpreted to mean x repeated n times (i.e., no internal compaction of the repetition is done).
Given a list of expressions e1, ..., em, which define elements a1, a2, ..., an that are all coercible into U, create the sequence Q = [ a1, a2, ..., an ] of elements of U.
Form the sequence of elements e(x), all belonging to some common structure, for those x ∈E with the property that the predicate P(x) is true. The expressions appearing in this construct have the interpretation given at the beginning of this section.If P(x) is true for every element of E, the sequence constructor may be abbreviated to [ e(x) : x in E ] .
Form the sequence of elements of U consisting of the values e(x) for those x∈E for which the predicate P(x) is true (an error results if not all e(x) are coercible into U). The expressions appearing in this construct have the same interpretation as above.
The sequence consisting of those elements e(x1, ..., xk), in some common structure, for which x1, ..., xk in E1, ..., Ek have the property that P(x1, ..., xk) is true.The expressions appearing in this construct have the interpretation given at the beginning of this section.
Note that if two successive ranges Ei and Ei + 1 are identical, then the specification of the ranges for xi and xi + 1 may be abbreviated to xi, xi + 1 in Ei.
Also, if P(x1, ..., xk) is always true, it may be omitted.
As in the previous entry, the sequence consisting of those elements e(x1, ..., xk) for which P(x1, ..., xk) is true is formed, as a sequence of elements of U (an error occurs if not all e(x1, ..., xk) are coercible into U).
Since enumerated sequences of integers arise so often, there are a few special constructors to create and handle them efficiently in case the entries are in arithmetic progression. The universe must be the ring of integers. Some effort is made to preserve the special way of storing arithmetic progressions under sequence operations.
The enumerated sequence of integers whose elements form the arithmetic progression i, i + 1, i + 2, ..., j, where i and j are (expressions defining) arbitrary integers. If j is less than i then the empty sequence of integers will be created.The universe U, if it is specified, has to be the ring of integers; any other universe will lead to an error.
The enumerated sequence consisting of the integers forming the arithmetic progression i, i + k, i + 2 * k, ..., j, where i, j and k are (expressions defining) arbitrary integers (but k≠0).If k is positive then the last element in the progression will be the greatest integer of the form i + n * k that is less than or equal to j; if j is less than i, the empty sequence of integers will be constructed.
If k is negative then the last element in the progression will be the least integer of the form i + n * k that is greater than or equal to j; if j is greater than i, the empty sequence of integers will be constructed.
The universe U, if it is specified, has to be the ring of integers; any other universe will lead to an error.
> s := [ IntegerRing(200) | x : x in [ 25..125 ] ];
A literal sequence is an enumerated sequence all of whose terms are from the same structure and all of these are `typed in' literally. The sole purpose of literal sequences is to load certain enumerated sequences very fast and very space-efficiently; this is only useful when reading in very large sequences (all of whose elements must have been specified literally, that is, not as some expression other than a literal), but then it may save a lot of time. The result will be an enumerated sequence, that is, not distinguished in any way from other such sequences.
At present, only literal sequences of integers are supported.
Given a succession of literal integers m1, ..., mn, build the enumerated sequence [m1, ..., mn], in a time and space efficient way.