/usr/share/axiom-20170501/src/algebra/FINITE.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 | )abbrev category FINITE Finite
++ Description:
++ The category of domains composed of a finite set of elements.
++ We include the functions \spadfun{lookup} and \spadfun{index}
++ to give a bijection between the finite set and an initial
++ segment of positive integers.
++
++ Axioms:\br
++ \tab{5}\spad{lookup(index(n)) = n}\br
++ \tab{5}\spad{index(lookup(s)) = s}
Finite() : Category == SIG where
SIG ==> SetCategory with
size : () -> NonNegativeInteger
++ size() returns the number of elements in the set.
index : PositiveInteger -> %
++ index(i) takes a positive integer i less than or equal
++ to \spad{size()} and
++ returns the \spad{i}-th element of the set.
++ This operation establishs a bijection
++ between the elements of the finite set and \spad{1..size()}.
lookup : % -> PositiveInteger
++ lookup(x) returns a positive integer such that
++ \spad{x = index lookup x}.
random : () -> %
++ random() returns a random element from the set.
enumerate : () -> List %
++ enumerate() returns a list of elements of the set
++
++X enumerate()$OrderedVariableList([p,q])
add
random() == index((1+random(size()$%))::PositiveInteger)
enumerate() == [index(i::PositiveInteger) for i in 1..size()]
|