Definitions StandardLib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No other cites to report in StandardLib
union1Def union1() == +Type+()
Thm* union1{i}()  Type{i'}
natDef  == {i:| 0i }
Thm*   Type
leDef AB == B<A
Thm* i,j:. (ij Prop
notDef A == A  False
Thm* A:Prop. (A Prop

Syntax:union1() has structure: union1{i:l}

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

Definitions StandardLib Sections NuprlLIB Doc