The Nuprl
system reads text from an edit window when that window is
closed by typing
. The text is read by a parsing routine which will
accept text that conforms to syntactic rules described in detail in section
8.1. These syntactic rules do not completely characterize the meaningful
entities; thus the parser may accept text which cannot be viewed as a term.
Essentially this means that the parser does not perform any type checking.
Text which is accepted by the parser is called
readable text. Text
which is meaningful in the sense of the semantic account in chapter 2 is
called readable and well--formed . Each well--formed
piece of text is called a
term. Note that our notion of well--formedness is semantic,
unlike the traditional usage of the word ``well-formed''.
The rest of this section
contains a brief discussion of syntactic issues that are of immediate
relevance.