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