Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
This is a list of selected documents from Nuprl Basics along with some theorems mentioned in them that are in some ways emblematic.

Pairs Thm* B:(AType), p:(u:AB(u)). p = <p.1,p.2>  a:AB(a)
Boolean Thm* p,q:. (pq p & q
Unit Thm* a:Unit. a = 
Disjoint Union Thm* z:A+Bz = InjCase(zu. inl(u); v. inr(v))
Equality Thm* (x.x) = (x.if x<0 0 ; x fi)  
Thm* (x.x (x.if x<0 0 ; x fi)  
Intersection Types Thm* B:(AType), a:A. (x:AB(x))  B(a)
Thm* A:Type, B:Type(given A). AB  Type
Quotient Types Thm* 2 = 4   mod 2
Void Thm* (x.whatever) = (x.x VoidA
Function Types Thm* f:(AB). (x.f(x)) = f
Thm* f,g:(AB). f = g  (x:Af(x) = g(x))
Polymorphism Thm* f:(( mod 2)A). f  A
Thm* T:Type, f:(D:Type. DT). f(f T
Thm* f:(D:Type. DT), A:Type, a:AB:Type, b:Bf(a) = f(b T
Thm* f:(C,D:Type. CDDC), A,B:Type, a:Ab:Bf(<a,b>) = <b,a BA
Thm* A  Top
Recursive Funs Thm* x:x 
Thm* mu  {f:()| x:f(x) }
Thm* A:Type, n:. (A^n Type
Recursive Types Thm* A:Type. Sexpr(A Type
Thm* a,b,c:X.
Thm* Reverse(Cons(Inj(a);Cons(Inj(b);Inj(c))))
Thm* =
Thm* Cons(Cons(Inj(c);Inj(b));Inj(a))
Propositions Thm* A,B:Prop. (A & B Prop
Thm* A:Type, P:(AProp). (x:AP(x))  Prop
High-Order Props Thm* A  B  (C:Prop. (A  C (B  C C)
Guarded Types Thm* A:Prop, B:Prop(given A). (A & B Prop
Type Functionality Thm* A,B:Type{i}. A+B  Type{i}
Thm* Type{i}  Type{i'}
Prop Levels Thm* Prop{i}  Type{i'}
Thm* Prop{i}  Prop{i'}
Thm* A,B:Prop{i}. (C:Prop{i}. (A  C (B  C C Prop{i'}
Type Conclusions Thm* x:( List){y:y greater-bounds x }
Restricted Decls Thm* k:x:(k List){y:(k+1)| y greater-bounds x }
Extraction Thm* ext{sfa_doc_find_intlist_great_bound}
Thm*  x:( List){y:y greater-bounds x }
Props as Types Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))
Thm* Dec(P (b:P  b)
Prop Witnesses Thm* x:y:yyx & x<(y+1)(y+1)

(Oct 2001 - sfa )

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

Definitions NuprlPrimitives Sections NuprlLIB Doc