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