next up previous contents index
Next: Syntactic Issues Up: Statements and Definitions Previous: Copying Text


  Nuprl provides a powerful and flexible definition facility which allows users to define their own notation. The general form of a definition follows:

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.

next up previous contents index
Next: Syntactic Issues Up: Statements and Definitions Previous: Copying Text

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995