Some definitions of interest.
fib	Def fib(n) == if n=0  n=1 1 else fib(n-1)+fib(n-2) fi  (recursive)
	Thm* n:. fib(n)
bor	Def p  q == if p true else q fi
	Thm* p,q:. (p  q)
coprime	Def CoPrime(a,b) == GCD(a;b;1)
	Thm* a,b:. CoPrime(a,b)  Prop
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
nat	Def  == {i:| 0i }
	Thm*   Type

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