IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Unit
This type has one value.
Thm* 
Unit
Thm* 
a:Unit. a =
It happens to be derived rather than primitive. See Deriving Unit.
There are many unit types of course, and this one has simply been adopted as a standard such type in by Nuprl users.
See Polymorphism about another basic unit type, "Top".
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
