Nat, Int, Real+, −, ∗, /, ^<=, >=, >, <..InfinityThe 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. <<3, 7>> \o <<3>> is equal to <<3, 7, 3>>.Head(s): The first element of the sequence s.Head(<<3,2,1>>) is equal to 3SelectSeq(s, Test): The subsequence of s consisting of the elements s[i] such that Test(s[i]) equals true.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(s, e): The sequence obtained by appending element e to the tail of sequence s. Append(<<3, 7>>, 3) equals <<3, 7, 3>>.Len(s): The length of sequence s. Len(<<1,2,3>>) is equal to 3.Seq(S): The set of all sequences of elements of the set S . Seq({3,7}) is equal to <<3, 7>>.Tail(s): The tail of sequence s, which consists of s with its head element removed.Tail(<<3, 7>>) equals <<7>>.IsFiniteSet(s): A set is finite iff there is a finite sequence containing all its elements.IsFiniteSet({1,2,3}) is equal to TRUECardinality(s): The number of elements in the set s. It's only defined for finite sets.Cardinality({1,2}) is equal to 2.(+), (-)BagInCopiesInSubBagBagOfAllEmptyBag\sqsubseteqBagToSetIsABagBagCardinalityBagUnionSetToBagRTBoundRTnownow:>, @@Print AssertJavaTimePermutationsSortSeq