Nuprl - Some Definitions

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

	Some definitions of interest.

next_nat_pair	Def next_nat_pair(xy) == xy/x,y. if y=0 <0,x+1> else <x+1,y-1> fi

	Thm* next_nat_pair

eq_int	Def i=j == if i=j true ; false fi

	Thm* i,j:. (i=j)

nat	Def == {i:\| 0i }

	Thm* Type

About:

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