SUC_CONV
reduceLib.SUC_CONV : conv
Calculates by inference the successor of a numeral.
If n is a numeral (e.g. 0, 1, 2, 3,...), then
SUC_CONV "SUC n" returns the theorem:
|- SUC n = s
where s is the numeral that denotes the successor of the natural
number denoted by n.
Failure
SUC_CONV tm fails unless tm is of the form "SUC n", where n is a
numeral.
Example
#SUC_CONV "SUC 33";;
|- SUC 33 = 34