(8steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
primrec
add
1
1.
T
: Type
2.
m
:
3.
b
:
T
4.
c
:
(0+
m
)
T
T
primrec(0+
m
;
b
;
c
) = primrec(0;primrec(
m
;
b
;
c
);
i
,
t
.
c
(
i
+
m
,
t
))
By:
Reduce 0
Generated subgoal:
1
primrec(0+
m
;
b
;
c
) = primrec(
m
;
b
;
c
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
T
primrec(0+m;b;c) = primrec(0;primrec(m;b;c);
i,t. c(i+m,t))
