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
)
sfa_doc_sexpr
Def
Sexpr(
A
) == rec(
T
.(
T
T
)+
A
)
Thm*
A
:Type. Sexpr(
A
)
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)+A)A:Type. Sexpr(A) TypeX:A. X B) & (X:B. X A)T)+A)A:Type. Sexpr(A) Type
