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_cons
Def
Cons(
s1
;
s2
) == inl(<
s1
,
s2
>)
Thm*
A
:Type,
s1
,
s2
:Sexpr(
A
). Cons(
s1
;
s2
)
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, s1,s2:Sexpr(A). Cons(s1;s2) Sexpr(A)T)+A)A:Type. Sexpr(A) TypeA:Type, s1,s2:Sexpr(A). Cons(s1;s2) Sexpr(A)
