1\DOC
2
3\TYPE {num_CONV : conv}
4
5\SYNOPSIS
6Equates a non-zero numeral with the form {SUC x} for some {x}.
7
8\EXAMPLE
9{
10- num_CONV ``1203``;
11> val it = |- 1203 = SUC 1202 : thm
12}
13
14\FAILURE
15Fails if the argument term is not a numeral of type {``:num``}, or if
16the argument is {``0``}.
17
18\SEEALSO
19numLib.SUC_TO_NUMERAL_DEFN_CONV.
20
21\ENDDOC
22