The Nuprl Basics documents explain the basic concepts and methods used for mathematical expression in Nuprl. The primitive operators as well as basic nonprimitives are discussed.

Structure.

These documents were generated according to three principles. First, they were generated progressively starting from the basic operators, and thereafter being generated as needed in order to continue the explanations. Second, concepts and notations that are standard were often used without first explaining them in type theoretic terms, in order not to clutter up the narrative; such elaboration is provided later in the explanations. Third, as what might be considered a corrolary of the second principle, the core theoretical connection between types and propositions was left unaddressed for as long as seemed practical. (Indeed, as of September 2003, the explanation of propositions-as-types is unfinished, but there is plenty explained independently of this.)

Thus, the overall effect is intended to be a progression from the ordinary and familiar towards more theoretically imbued explanations.

In addition to the links within pages to narratively "adjacent" ones there are, appended to each page, links to the documents explaining basic operators that occur on the page. These links are displayed as instances of those operators.

Nuprl Basics contains a list of the main documents in a reasonable reading order. An approximate size in words is indicated for each, indicating a certain kind of emphasis.

Citations. I'll add them later.

Printed copies.
There is a print version (circa 70pp) (postscript) of the finished documents with cross-references, and a longer one (circa 120pp) (postscript) including mentioned proofs. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html