WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sfa
doc
sexpr
inj?
sfa_doc_sexpr_inj
Def Inj(
a
) == inr(
a
)
Thm*
A
:Type,
a
:
A
. Inj(
a
)
Sexpr(
A
)
Syntax:
Inj(
a
)
has structure:
sfa_doc_sexpr_inj(
a
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc