Definitions
hol
arithmetic
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
Thm*
S
odd
Def
odd(
n
) == if
n
=
0 then false
else
odd(
n
-1) fi (recursive)
Thm*
n
:
. odd(
n
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
hol
arithmetic
1
Sections
HOLlib
Doc
== {i:
| 0
i } 
Type S
0 then false else 
odd(n-1) fi (recursive)
n:. odd(n) 
== {i:| 0i } Type S0 then false else odd(n-1) fi (recursive)n:. odd(n) 
