Standard Library
Modules ''Naturals'', ''Integers'', ''Reals''
Nat
,Int
,Real
+
,−
,∗
,/
,^
<=
,>=
,>
,<
..
Infinity
Module ''Sequences''
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 to3
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 ifm < 1
orn > Len(s)
, except that it equals the empty sequence ifm > n
.Append(s, e)
: The sequence obtained by appending element e to the tail of sequence s.- Example:
Append(<<3, 7>>, 3)
equals<<3, 7, 3>>
.
Len(s)
: The length of sequence s.- Example:
Len(<<1,2,3>>)
is equal to3
.
Seq(S)
: The set of all sequences of elements of the set S .- Example:
Seq({3,7})
is equal to<<3, 7>>
.
Tail(s)
: The tail of sequences
, which consists ofs
with its head element removed.- Example:
Tail(<<3, 7>>)
equals<<7>>
.
Module ''FiniteSets''
IsFiniteSet(s)
: A set is finite iff there is a finite sequence containing all its elements.- Example:
IsFiniteSet({1,2,3})
is equal toTRUE
Cardinality(s)
: The number of elements in the set s. It's only defined for finite sets.- Example:
Cardinality({1,2})
is equal to 2.
Module ''Bags''
(+)
,(-)
BagIn
CopiesIn
SubBag
BagOfAll
EmptyBag
\sqsubseteq
BagToSet
IsABag
BagCardinality
BagUnion
SetToBag
Module ''RealTime''
RTBound
RTnow
now
Module ''TLC''
:>
,@@
Print
Assert
JavaTime
Permutations
SortSeq