The category of domains composed of a finite set of elements. We include the functions lookup and index to give a bijection between the finite set and an initial segment of positive integers.
- enumerate: () -> List %
enumerate()returns list of elements of the set.
- index: PositiveInteger -> %
index(i)takes a positive integer
iless than or equal to
size()and returns the
-th element of the set. This operation establishes a bijection between the elements of the finite set and
- lookup: % -> PositiveInteger
lookup(x)returns a positive integer such that
x = index lookup x.
- random: () -> %
random()returns a random element from the set.
- size: () -> NonNegativeInteger
size()returns the number of elements in the set.