WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sfa
doc
ntuple?
sfa_doc_ntuple
Def
A
^
n
== if
n
=
0
Unit ;
n
=
1
A
else
A
(
A
^(
n
-1)) fi (recursive)
Thm*
A
:Type,
n
:
. (
A
^
n
)
Type
eq_int
Def
i
=
j
== if
i
=
j
true
; false
fi
Thm*
i
,
j
:
. (
i
=
j
)
Syntax:
A
^
n
has structure:
sfa_doc_ntuple(
A
;
n
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc