Typical lesson material consists of documents blending formal with informal text which are intended to be read with an interactive browser. One particularly useful hypertext link is one that points to a proof of a theorem. One may, of course, create an ordinary hypertext link to a proof, but often it is more convenient to show the content of the theorem at its point of use, and so Nuprl includes links that display content. For example:
When the user clicks on this, the formal proof, or a document informally glossing it, is opened for viewing. Such a link to a theorem may be embedded in informal hypertext, and may also be used within proofs of other theorems that use it as a lemma. How formal proofs are read will be discussed in the next section. Another example of these links that display content are the references to definitions such as:
Not only do links of this kind enable the user to track down references, but they also prevent documentation from getting out of ``sync'' should the objects or notations get modified.
definitions and blending materials
The ability to find the definition of an operator from any use
of it throughout the system is a key feature of the Nuprl editor.
For example,
if the user wanted to see the definition of ``divides,'' he or she could
click on any occurrence of it, such as ``na | n
b'', and the defi
nition would be viewed, which looks like this:
It is also possible to associate other documentation with the definition which will be presented when the definition is viewed, such as informal descriptions and links to related lessons. Such occurrences of the ``divides'' operator are formal no matter where they occur, either in proofs or in informal documents. Besides the benefit of being able to find the definition, if the user wants to change the way an operator is displayed, say to ``x divides y'' instead of ``x | y'', this change will be automatically adopted throughout the system since it is the abstract expression rather than the text ``x | y'' that is used.
Formal and informal material can be freely mixed. If this proposal had been presented on the Nuprl system, for example, you could actually have clicked on the theorem references and operator occurrences occurring above with the described effects. So one can write informally about a subject but use the formal notations whenever desired, thus allowing the user full access to relevant formal materials such as definitions and proofs, and any other documentation that has been attached to the formal materials. Conversely, one can insert commentary inside the formal objects of the system.
structure editing Formal mathematical notations are edited with a visually oriented structure editor [63]. It is a structure editor rather than a text editor because we edit the abstractly represented term directly rather than a string of characters that gets parsed into a term. The editor is visually oriented in that the interpretation of most edit commands depends not only upon the abstract term structure, but also, of course, on the display forms in use. Most of this editing is performed by means of cut-and-paste operations and various menus, so it is not necessary for the students to master a large ``name space'' for commands, operators, and library objects.
some conventional notational devices supported by Nuprl It often happens that when you develop a body of mathematics, you find you have implicitly parameterized it by one or more variables held fixed throughout large expressions. In Nuprl, these implicit parameters would fill actual argument places in the underlying term, which would be elided during display; but if filled by some other expressions, these places would be shown.
Another conventional notational device is to abbreviate the display of certain iterated operators.
The larger point is that we respect conventional notations, which we must suppose have often developed for good reason. When we can, and can afford to, we try to adopt conventional devices into our system. The obstacles in any case are figuring out how the notation works, and determining whether it is compatible with prior systematic constraints on formal expression we have established for Nuprl.