Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
sfa_doc_exteq
Def
A
=ext
B
== (
X
:
A
.
X
B
) & (
X
:
B
.
X
A
)
singleton
Def
{
a
:
T
} == {
x
:
T
|
x
=
a
T
}
Thm*
T
:Type,
a
:
T
. {
a
:
T
}
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
X:A. X 
B) & (X:B. X A) T }T:Type, a:T. {a:T} TypeX:A. X B) & (X:B. X A) T }T:Type, a:T. {a:T} Type
