Nuprl - Some Definitions

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

	Some definitions of interest.

ndiff	Def a -- b == imax(a-b;0)

	Thm* a,b:. (a -- b)

imax	Def imax(a;b) == if ab b else a fi

	Thm* a,b:. imax(a;b)

imin	Def imin(a;b) == if ab a else b fi

	Thm* a,b:. imin(a;b)

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

	Thm* Type

About:

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