Selected Objects

def	nnsub	nnsub(m;n) == if m<n then 0 else m-n fi
THM	nnsub_nuprl	m,n:. mn  nnsub(n;m) = n-m
def	exp	exp(m;n) == if n=0 then 1 else mexp(m;n-1) fi   (recursive)
THM	exp_zero	m:. exp(m;0) = 1
THM	exp_pos	m,n:. n>0  exp(m;n) = mexp(m;n-1)
def	fact	fact(n) == if n=0 then 1 else nfact(n-1) fi   (recursive)
THM	fact_zero	fact(0) = 1
THM	fact_pos	n:. n>0  fact(n) = nfact(n-1)
def	even	even(n) == if n=0 then true else even(n-1) fi   (recursive)
THM	even_zero	even(0) = true
THM	even_pos	n:. n>0  even(n) = even(n-1)
def	odd	odd(n) == if n=0 then false else odd(n-1) fi   (recursive)
THM	odd_zero	odd(0) = false
THM	odd_pos	n:. n>0  odd(n) = odd(n-1)
def	nmod	nmod(m;n) == if n=0 then 0 else m rem n fi
def	ndiv	ndiv(m;n) == if n=0 then 0 else m  n fi
def	hadd	add == m:. n:. m+n
def	hsub	sub == m:. n:. nnsub(m;n)
def	hmult	mult == m:. n:. mn
def	hexp	exp == m:. n:. exp(m;n)
def	hgt	gt == m:. n:. n<m
def	hle	le == m:. n:. mn
def	hge	ge == m:. n:. nm
def	hfact	fact == n:. fact(n)
def	heven	even == n:. even(n)
def	hodd	odd == n:. odd(n)
def	hmod	mod == m:. n:. nmod(m;n)
def	hdiv	div == m:. n:. ndiv(m;n)

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