Nuprl - Some Definitions

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

	Some definitions of interest.

hanoi_PEG	Def Peg == {1...3}

	Thm* Peg Type

iff	Def P Q == (P Q) & (P Q)

	Thm* A,B:Prop. (A B) Prop

int_iseg	Def {i...j} == {k:\| ik & kj }

	Thm* i,j:. {i...j} Type

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

	Thm* Type

nequal	Def a b T == a = b T

	Thm* A:Type, x,y:A. (x y) Prop

About:

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