Nuprl - Some Definitions

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

	Some definitions of interest.

comment	Def Kind of comment: $kind == a

gt	Def i>j == j<i

	Thm* i,j:. (i>j) Prop

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

	Thm* Type

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

	Thm* Type

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

	Thm* a:. prime(a) Prop

About:

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