The call dest_small_numeral t where t is the HOL numeral representation of
n, returns n as an OCaml machine integer. It fails if the term is not a
numeral or the result doesn't fit in a machine integer.
FAILURE CONDITIONS
Fails if the term is not a numeral or if the result doesn't fit in a machine
integer.
EXAMPLE
# dest_small_numeral `12`;;
val it : int = 12
# dest_small_numeral `18446744073709551616`;;
Exception: Failure "int_of_big_int".
COMMENTS
If overflow is a danger, you may be better off using OCaml type num and the
analogous function dest_numeral. However, none of HOL's inference rules
depend on the behaviour of machine integers, so logical soundness is not an
issue.