Nuprl - Some Definitions

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

	Some definitions of interest.

hlist	Def hlist('a) == 'a List

	Thm* 'a:S. hlist('a) S

hnum	Def hnum ==

	Thm* hnum S

label	Def t ...$L == t

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

	Thm* Type

	Thm* S

not	Def A == A False

	Thm* A:Prop. (A) Prop

stype	Def S == {T:Type\| x:T. True }

	Thm* S Type{2}

About:

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