NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
CONTINUED from primitive op doc HISTORY

March 2001

Completed Proof Witness Extraction.
Added Sequents with Type Conclusions, Sequents with Restricted Declarations.
Reworked Sequents a bit punting to Sequents with Type Conclusions.
Mentioned polymorphism and gave an example in Intersection Types
Added Propositions as Types - standard defs which really needs support from further explanations.
Alluded to Comprehension Subtypes and Quotient Types in Types.
Described equality between quotient type expressions in Quotient Types and alluded to it in Intensional Types.
Reordered entries in primitive op doc INDEX to make it closer to order of understanding.
Made some of the structure of the Operator Definition document explicit.
Improved the wording in Evaluation and Term Rewriting about marking subterms for rewriting.
In NonCanonical Forms, removed the <term> marks, and added mention of principal argument place.
In Terms, added an example of 2-place snd-o var instance, and deleted line about creation of new expressions.
Reworded Russell's Orders to make it clear that a sequence of orders was being described.
Eliminated from Equality references to props as types.
Added some detailed reminders to previous info Type Expressions.
Added mention of typing Kleene's mu operator to Recursive Functions.
Some subtypes of were mentioned in Integers.

Feb 2001

The bulk of the documentation, down to but excluding computational content of propositions and choice principles, written in February 2001. Citations are to be added later. Here are the documents then considered complete:

Pairs Boolean
Atoms Negative Literals
Disjoint Union Deriving Bool
Lists Unit
Void Deriving Unit
Integers Recursive Functions
Quotient Types Recursion via the Y-combinator
Comprehension Subtypes Y-combinator Continued
Equality Multi-argument Functions with Y
Intersection Types Recursive Types
Guarded Types Terms
Types Operator Definition
Intensional Types Op Def Restrictions
Computation Substitution
Evaluation and Term Rewriting Canonical Forms
Universes NonCanonical Forms
Propositions Type Expressions
Functions Proofs
Function Types Propositions as Types
Multi-Argument Functions Prop Levels and Predicativity
Functionality Sequents Higher-Order Propositions
Sequents ML
Type Functionality Sequents Russell's Orders

The incomplete documents these refer to are Choice(incomplete) and Computational Content(incomplete).

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

NuprlPrimitives Sections NuprlLIB Doc