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+B. z = InjCase(z; u. 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:A. B(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:A. f(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:A, B:Type, b:B. f(a) = f(b)  T Thm* f:(C,D:Type. CDDC), A,B:Type, a:A, b:B. f(<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:A. P(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)

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