Nuprl - Some Definitions

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

	Some definitions of interest.

prime_nats	Def Prime == {x:\| prime(x) }

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

	Thm* Type

prime_mset_complete	Def prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi

	Thm* f:(Prime). prime_mset_complete(f)

About:

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