num_CONV : conv
STRUCTURE
numLib
SYNOPSIS
Equates a non-zero numeral with the form
SUC x
for some
x
.
EXAMPLE
- num_CONV ``1203``; > val it = |- 1203 = SUC 1202 : thm
FAILURE
Fails if the argument term is not a numeral of type
``:num``
, or if the argument is
``0``
.
SEEALSO
SUC_TO_NUMERAL_DEFN_CONV
HOL
Kananaskis-14