Conventions

We give the conventions we use in this manual for presenting user input and Nuprl output.

Input which you should type is presented typewriter font. For example this is in typewriter font. The following symbols are also used:

• SPACE for the space-bar .
• RETURN for the return key  (sometimes marked as ``enter'').
• LINEFEED for the linefeed key .
• TAB for the tab key TAB }.
• DELETE for the delete key  (sometimes marked as rubout). On some keyboards the BACKSPACE   has the same effect.
• MOUSE-LEFT   for the left mouse button.
• MOUSE-MIDDLE   for the middle mouse button.
• MOUSE-RIGHT   for the right mouse button.

Modified keys  are presented as follows:

• C- X   read as ``control  x''. Hold down a control key and simultaneously press key x.
• M- X   read as ``meta  x''. Hold down a meta key and simultaneously press key x.
• CM- X   read as ``control meta  x''. Hold down both a control key and a meta key, and simultaneously press key x.
• S- X   read as ``shift x''. Hold down a shift key and simultaneously press key x.

Note that x is either a keyboard key or a mouse button; for example both C-A and M- MOUSE-RIGHT are valid modified keys.. On some keyboard's (for example, those of Sparc-stations) the usual meta keys are the keys marked either side of the space-bar. The S- X modifier is only used with non-printing characters 

(for example, RETURN ).

When we say ``click MOUSE-LEFT '' on some part of a window, we mean that the mouse cursor should be pointed at that part, and then the MOUSE-LEFT button should be pressed.

Be aware that Nuprl can be quite slow to respond to keystrokes, sometimes taking several seconds. Don't hold keys down till you get a response. You might easily make the keys autorepeat  , which could be rather annoying.

For clarity when presenting input which a user might type, or output which Nuprl generates, we sometimes enclose the input  or output  text in special quotes . For example this is example output .

Some cursors in Nuprl highlight a part of window. The highlighting is indicated on the screen by swapping the foreground and background colors of the display. For example, if normally the display has black characters on a white background , then a highlighted part has white characters on a black background. In this document we indicate a highlighted region of the screen by drawing an outline around it. For example, in the window

the [int] * [int] is considered to be highlighted.