TLA+ Wiki

This is an old revision of the document!

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

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:
```
PosSubSeq(s) == LET IsPos(n) == n > 0
                in SelectSeq(s, IsPos)
```
  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
Len
Seq(S): The set of all sequences of elements of the set S .
- Example: Seq({3,7}) is equal to <<3, 7>>.
Tail