Nuprl - Some Definitions

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

	Some definitions of interest.

habs_num	Def abs_num == n:. @m:. (n = rep_num(m) )

	Thm* abs_num (hind hnum)

hrep_num	Def rep_num == n:. ncompose(suc_rep;n;zero_rep)

	Thm* rep_num (hnum hind)

choose	Def @x:T. P(x) == InjCase(lem({x:T\| P(x) }); x. x, arb(T))

	Thm* T:S, P:(TType). (@x:T. P(x)) T

hnum	Def hnum ==

	Thm* hnum S

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

	Thm* Type

	Thm* S

About:

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