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_sexpr
Def
Sexpr(
A
) == rec(
T
.(
T
T
)+
A
)
Thm*
A
:Type. Sexpr(
A
)
Type
sfa_doc_sexpr_inj
Def
Inj(
a
) == inr(
a
)
Thm*
A
:Type,
a
:
A
. Inj(
a
)
Sexpr(
A
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
T)+A)
A:Type. Sexpr(A) 
TypeA:Type, a:A. Inj(a) Sexpr(A)T)+A)A:Type. Sexpr(A) TypeA:Type, a:A. Inj(a) Sexpr(A)
