next up previous contents index
Next: Theorems Up: Statements and Definitions Previous: Definitions

Syntactic Issues


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.

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