NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Unit is derived rather than primitive.

This type has one value.

Thm*   Unit

Thm* a:Unit. a = 

There happen already to be other single element types. Propositions expressing equality and membership propositions are often represented as types that have a member iff they are true, and when they are true, the sole member is "*".
See Propositions

Def Unit == 0  

Def  == *

Thm* a:(0  ). a = *

(Feb 2001 - sfa )

About:
unititintnatural_numberequalaxiommemberall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

NuprlPrimitives Sections NuprlLIB Doc