The left--hand side of a definition gives the form in which the definition is
displayed
when invoked; it gives the syntax of the extended notation. The right--hand
side expresses the meaning of the new notation in terms of existing notation.
The occurrences of <formal name:description> are
parameters of the new notation. It is essential to use the angle brackets
to enclose the parameters of a definition; otherwise, the symbol intended as
a parameter will be used as a literal symbol every time the definition is
instantiated.
If the left angle
bracket, <, is used as the less than symbol of number theory then
it must be preceded by an escape character, 
in the text editor, to prevent
the system from interpreting the < as the start of a parameter to the
definition.
Most of the definitions shown in this chapter have
the escape character removed in order to make the definitions more readable.
A definition is created in much the same way as a theorem is created. One opens a place in the library using the command create name def place. The object is then viewed by the command view name, which in the case of a definition invokes the text editor rather than the proof editor. The form of the definition is now entered directly in the text editor. To illustrate this process suppose one wishes to define the logical connective ``and'' in terms of the type constructor #. A place in the library is first created using the create command; this command would include a name, say and, for the definition being created. The object and would then be viewed, and the text editor would thereby be invoked. In the text editor one would type
<p:prop> & <q:prop> == ( (<p>) # (<q>) ).Upon exit with
the system places the definition in the library.
Before a
definition can be used it must be checked ; this is
done by issuing the command check name-of-def .
The system updates the status of the
definition to either good, indicated by the
status mark 
, or bad,
indicated by the status mark --.
Returning to our example, after and is checked, it extends the
notation by introducing the new symbol &, which is defined in terms
of the existing type constructor #.
To use a definition in creating another object, one types
in the text editor while editing the new object;
the cursor
will be put in the command window with the prompt being I>. The definition
name is typed followed by a RETURN
; the left--hand side of the definition appears
where the cursor is positioned. Angle brackets containing the description
will appear in the positions where a parameter is expected. In the example
above, using the definition would result in the appearance of
[<prop> & <prop> ].
The parameters, p and q in the example
above, can
now be entered by moving the cursor to the places indicated by angle
brackets and typing the desired parameters. As the instantiations for the
parameters are typed the angle brackets vanish.
It is possible to use another definition while instantiating
the parameters of a definition.
If one wishes to delete a definition then
the kill command must be used.
To delete an instance of a definition in another object, one
positions the cursor at the beginning of the definition and hits the kill key.
The easiest way to ensure that the cursor is correctly
positioned is to use bracket mode. This is a
display mode in which
instantiated definitions are shown with brackets surrounding them
and is normally the
default mode. If the bracket display is not desired,
bracket mode can be turned off by using 
. This key serves as a
toggle between the two display modes.