WhoCites
Definitions
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites primrec?
primrec
Def primrec(
n
;
b
;
c
) == if
n
=
0
b
else
c
(
n
-1,primrec(
n
-1;
b
;
c
)) fi (recursive)
Thm*
T
:Type,
n
:
,
b
:
T
,
c
:(
n
T
T
). primrec(
n
;
b
;
c
)
T
eq_int
Def
i
=
j
== if
i
=
j
true
; false
fi
Thm*
i
,
j
:
. (
i
=
j
)
Syntax:
primrec(
n
;
b
;
c
)
has structure:
primrec(
n
;
b
;
c
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
list
2
Sections
MarkB
generic
Doc