(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
sexpr
fp
A
:Type. Sexpr(
A
) =ext (Sexpr(
A
)
Sexpr(
A
))+
A
By:
Auto
Generated subgoals:
1
1.
A
: Type
2.
X
: Sexpr(
A
)
X
(Sexpr(
A
)
Sexpr(
A
))+
A
2
steps
2
1.
A
: Type
2.
X
: (Sexpr(
A
)
Sexpr(
A
))+
A
X
Sexpr(
A
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
A:Type. Sexpr(A) =ext (Sexpr(A)
Sexpr(A))+A A:Type. Sexpr(A) =ext (Sexpr(A)Sexpr(A))+A X 
(Sexpr(A)Sexpr(A))+A
Sexpr(A))+A
X Sexpr(A)
