Rule definitions are expressed as `terms' in the sense described in
Chapter 
. They are normally stored in library objects of kind
rule .
Figure
shows the basic tree structure of rule terms.
I have included kinds of `virtual tree nodes' in this description.
These virtual nodes do not correspond to term constructors used in
building up rules, but they do help in explaining the structure of
rule terms
.
Italic type is used in Figure
for kinds of tree nodes
that correspond to terms and term slots
. Roman type is used for tree
nodes that correspond to text strings and text slots .
indicates a linebreak in a display form,
null
indicates a display form with `zero width' , and
is the usual invisible
space. The suffix * character on a node-kind names indicate a
sequence of nodes. The prl-term node kind is for terms in Nuprl
's
object language.
Names for the term constructors that are suitable for entering the
constructors are shown in the `alias' column. The term constructors
for sequences do not need to be entered explicitly by name. The
editor recognizes the context of each sequence, and sequence items can
be added and deleted using the 
C-O
and 
C-C
sequence
commands.
For rule terms to be well-formed, there are several extra constraints on their structure. These include:
