Nuprl - Some Definitions

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

	Some definitions of interest.

prime	Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a \| bc a \| b a \| c)

	Thm* a:. prime(a) Prop

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

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

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

	Thm* Type

About:

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