Some definitions of interest.
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
decidable	Def Dec(P) == P  P
	Thm* A:Prop. Dec(A)  Prop
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
sfa_doc_greater_list_bound	Def y greater-bounds x == i:||x||. x[i]<y
	Thm* x: List, y:. y greater-bounds x  Prop
int_seg	Def {i..j} == {k:| i  k < j }
	Thm* m,n:. {m..n}  Type
kleene_minimize	Def mu(f) == if f(0) 0 else 1+mu(x.f(1+x)) fi  (recursive)
	Thm* mu  {f:()| x:. f(x) }
nat	Def  == {i:| 0i }
	Thm*   Type
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
nequal	Def a  b  T == a = b  T
	Thm* A:Type, x,y:A. (x  y)  Prop
sfa_doc_factorial	Def x! == if x=0 1 else x(x-1)! fi  (recursive)
	Thm* x:. x!
sfa_doc_ntuple	Def A^n == if n=0 Unit ; n=1 A else A(A^(n-1)) fi  (recursive)
	Thm* A:Type, n:. (A^n)  Type
sfa_doc_sample_intmod	Def  mod k == x,y://(m:. x-y = mk)
	Thm* k:.  mod k  Type
sfa_doc_sexpr	Def Sexpr(A) == rec(T.(TT)+A)
	Thm* A:Type. Sexpr(A)  Type
sfa_doc_sexpr_reverse	Def Reverse(e) Def == Case of e Def == CaInj(x)  Inj(x) Def == CaCons(s1;s2)  Cons(Reverse(s2);Reverse(s1)) Def (recursive)
	Thm* A:Type, e:Sexpr(A). Reverse(e)  Sexpr(A)
sfa_doc_sexpr_cons	Def Cons(s1;s2) == inl(<s1,s2>)
	Thm* A:Type, s1,s2:Sexpr(A). Cons(s1;s2)  Sexpr(A)
sfa_doc_sexpr_inj	Def Inj(a) == inr(a)
	Thm* A:Type, a:A. Inj(a)  Sexpr(A)
subtype	Def S  T == x:S. x  T
top	Def Top == Void(given Void)
	Thm* Top  Type

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