Precedence objects collectively introduce a set of precedence elements, and define a partial order on them.
Table: Precedence Object Elements
Table
shows the components of a precedence
object, and the names used to enter them by. The par, ser, and
eq terms are sequence constructors so the standard sequence commands
work on the sequences built with these terms.
Each display form not explicitly associated with any precedence element is implicitly associated with a unique precedence element unrelated to all other precedence elements. The uniqueness implies that two such display forms have unrelated precedence.
The core_1 theory should be consulted to see how a base set of precedences has been set up for the current Nuprl theories.