| Next revision | Previous revision |
| using:standard_lib [2024/09/28 15:58] – created - external edit 127.0.0.1 | using:standard_lib [2024/10/10 16:42] (current) – fponzi |
|---|
| ====== Standard Library ====== | ====== 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 to ''3'' |
| | * ''SelectSeq(s, Test)'': The subsequence of s consisting of the elements s[i] such that Test(s[i]) equals true. |
| | * Example: <code latex>PosSubSeq(s) == LET IsPos(n) == n > 0 |
| | in SelectSeq(s, IsPos)</code> 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. |
| | * Example: ''Append(<<3, 7>>, 3)'' equals ''<<3, 7, 3>>''. |
| | * ''Len(s)'': The length of sequence s. |
| | * Example: ''Len(<<1,2,3>>)'' is equal to ''3''. |
| | * ''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 sequence ''s'', which consists of ''s'' 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 to ''TRUE'' |
| | * ''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'' |
| |
127.0.0.1