Some definitions of interest.
flip	Def (i, j)(x) == if x=i j ; x=j i else x fi
	Thm* k:, i,j:k. (i, j)  kk
int_seg	Def {i..j} == {k:| i  k < j }
	Thm* m,n:. {m..n}  Type
nat	Def  == {i:| 0i }
	Thm*   Type
sum	Def sum(f(x) | x < k) == primrec(k;0;x,n. n+f(x))
	Thm* n:, f:(n). sum(f(x) | x < n)
primrec	Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi  (recursive)
	Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c)  T

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