IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
NuprlPrimitives
Nuprl Section: NuprlPrimitives - Explanations of Nuprl Primitives and Conventions

Basic Nuprl Documentation

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

Below is 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. There is also a partial index to these documents by Emblematic Theorems, some of which are quite interesting.

Main Documents Created as of September 2003 - sfa:

 Pairs 210 words Lists 230 words Boolean (Deriving Bool) 290 (20) words Unit (Deriving Unit) 50 (60) words Integers (Negative Literals) 160 (160) words Atoms 290 words Disjoint Union 140 words Comprehension Subtypes 70 words Types 760 words Type Expressions 430 words Intensional Types 390 words Universes 390 words Equality 250 words Intersection Types 240 words Quotient Types 130 words Void 170 words Functions 590 words Function Types 380 words Polymorphism 490 words Multi-Argument Functions 280 words Recursive Functions 220 words Recursion via the Y-combinator 210 words Y-combinator Continued 340 words Typing Y 310 words Typing Y Continued 250 words Multi-argument Functions with Y 170 words Recursive Types 270 words Propositions 360 words Higher-Order Propositions 320 words Guarded Types 180 words Functionality Sequents 290 words Type Functionality Sequents 510 words Prop Levels and Predicativity 350 words Russell's Orders 330 words Terms 340 words Computation 360 words Canonical Forms 60 words NonCanonical Forms 140 words Evaluation and Term Rewriting 310 words "Squiggle" Operator 400 words Operator Definition 210 words Substitution 480 words Op Def Restrictions 420 words Sequents 430 words Proofs 530 words ML 70 words Sequents with Type Conclusions 280 words Sequents with Restricted Declarations 320 words Proof Witness Extraction 270 words Propositions as Types 520 words Propositions as Types - standard defs 160 words Propositional Proof Witness Extraction 340 words
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html