NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /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.

See Structure, Principles and Printed Copies of the Basic Documents.

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 /sfa/Nuprl/Shared/Xindentation_hack_doc.html

NuprlPrimitives Sections NuprlLIB Doc