Some definitions of interest.
length	Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
nat	Def  == {i:| 0i }
	Thm*   Type
sfa_doc_inlist	Def a list xs == Case of xs; nil  False ; x.ys  x = a  A  a list ys Def (recursive)
	Thm* A:Type, a:A, xs:A List. (a list xs)  Prop
sfa_doc_sample_intmod	Def  mod k == x,y://(m:. x-y = mk)
	Thm* k:.  mod k  Type
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