PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
ntuple
is
prod
A
:Type,
n
:
.
n
2
(
A
^
n
) =
A
(
A
^(
n
-1))
By:
Auto
THEN
Compute
A
^
n
*
if
n
=
0
Unit ;
n
=
1
A
else
A
(
A
^(
n
-1)) fi
THEN
Repeat (SplitITE Concl)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
A:Type, n:
. n
2 
(A^n) = A
(A^(n-1)) A:Type, n:. n2 (A^n) = A(A^(n-1)) if n=
0
Unit ; n=1 A else A(A^(n-1)) fi
