Nuprl - Some Definitions

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

	Some definitions of interest.

divides	Def b \| a == c:. a = bc

	Thm* a,b:. (a \| b) Prop

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

	Thm* Type

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

	Thm* Type

nat_plus	Def == {i:\| 0<i }

	Thm* Type

About:

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