/usr/share/axiom-20170501/src/algebra/ORDSET.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 43 44 45 46 47 48 | )abbrev category ORDSET OrderedSet
++ Description:
++ The class of totally ordered sets, that is, sets such that for each
++ pair of elements \spad{(a,b)}
++ exactly one of the following relations holds \spad{a<b or a=b or b<a}
++ and the relation is transitive, that is, \spad{a<b and b<c => a<c}.
OrderedSet() : Category == SIG where
SIG ==> SetCategory with
"<" : (%,%) -> Boolean
++ x < y is a strict total ordering on the elements of the set.
">" : (%, %) -> Boolean
++ x > y is a greater than test.
">=" : (%, %) -> Boolean
++ x >= y is a greater than or equal test.
"<=" : (%, %) -> Boolean
++ x <= y is a less than or equal test.
max : (%,%) -> %
++ max(x,y) returns the maximum of x and y relative to "<".
min : (%,%) -> %
++ min(x,y) returns the minimum of x and y relative to "<".
add
x,y: %
-- These really ought to become some sort of macro
max(x,y) ==
x > y => x
y
min(x,y) ==
x > y => y
x
((x: %) > (y: %)) : Boolean == y < x
((x: %) >= (y: %)) : Boolean == not (x < y)
((x: %) <= (y: %)) : Boolean == not (y < x)
|