Nuprl Basics - primitive op doc HISTORY

Definitions NuprlPrimitives Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
These documents were written by sfa as a supplement to the Nuprl Library. When reading the library in progressively greater detail, one rather quickly hits upon Nuprl primitives and expressive methods that should be explained. These documents were generated by documenting the primitive type constructors, which engendered further descriptions progressively down to type theory. The design is to forestall explanation of essentially type-theoretic issues as long as possible, to emphasize the higher level ordinary expression of mathematics.

September 2003

Added to Proofs a remark about negative hyp number references.
Added some paraphrases for the standard propositional ops in Propositions.
Reworked Propositions as Types to incorporate a brief treatment of computational content and dropped its references to the merely planned pages about it; also adjusted Propositions as Types - standard defs, Propositions, and Propositional Proof Witness Extraction similarly.

August 2003

Began reformatting documents to make the more suitable as printable pages.

January 2003

Added a document Subtyping Relation about advance adoption of the subtype relation primitive.
Added a new extensional fixedpoint theorem
Thm* A:Type. Sexpr(A) =ext (Sexpr(A)Sexpr(A))+A
to Recursive Types (a note from Kreitz prompted this).

November 2002

Added to Operator Definition indication that function applications, "<fun>(<arg>)" can be used on the lhs of an opdef instead of lambdas, "[var].<*>", on the rhs.
Added a new theorem about polymorphic functions
Thm* f:(D:Type. DT), A:Type, a:A, B:Type, b:B. f(a) = f(b) T
to Polymorphism ( Barzilay suggested adding this).

December 2001

Corrected an erroneous inl(b) to inr(b) in Computation.
Indicated rec(X.(X)) as an example failure of type formation in Recursive Types.

October 2001

Added a reference to Thm* whatever1 = whatever2 (x:Void. Whatever(x)) in Intersection Types.
Added a mention of Dec(P) to Propositions as Types.
Added Thm* Dec(P) (b:. P b) to primitive ops emblem thms for Props as Types.

September 2001

Corrected some small errors in Polymorphism, and added more thms as examples.
Added a thm citation to Pairs.
Added some thm citations to Lists.
Added a thm citation and some material about outl,inl,isl to Disjoint Union.
Added a thm citation to Intersection Types
Added a thm citation to Quotient Types.
Added some thm citations about extensionalty to Function Types.
Added Typing Y and Typing Y Continued about how to type the Y combinator if we extend the Function Extensionality rule.
Added primitive ops emblem thms (partial index to documents by emblamatic theorem).

August 2001

Moved the reference to Void in Nuprl Basics.
Added much more material to Void.
Added Polymorphism.
Added references to Top to Unit, Intersection Types, Quotient Types.
Added Subtype Relation.
Added reference to Subtype Relation to Type Expressions.
Added "Squiggle" and linked to it from Types.

May 2001

In Boolean added a demonstration of where implicit -to-Prop coercions occurred in Thm* p,q:. (pq) p & q.
In Prop Levels and Predicativity changed "predicative logic" to "predicative semantics".
I changed the suggested reading order of Substitution and Op Def Restrictions in Nuprl Basics.
In Op Def Restrictions, I eliminated a true but distracting parenthetical comment about the left hand side not being too general. I also glossed "second-order variable" as a link.
Added a caveat to Functions to not identify computational evaluation with an expressions standing for a value.
Added a missing condition to Op Def Restrictions, namely "Distinct subterm positions of the left-hand side must be filled by distinct variables."
Corrected Universes to use as domain of V(i) instead of .