mk_numeral : num -> term

SYNOPSIS
Maps a nonnegative integer to corresponding numeral term.

DESCRIPTION
The call mk_numeral n where n is a nonnegative integer of type num (this is OCaml's type of unlimited-precision numbers) returns the HOL numeral representation of n.

FAILURE CONDITIONS
Fails if the argument is negative or not integral (type num can include rationals).

EXAMPLE
  # mk_numeral (Int 10);;
  val it : term = `10`

  # mk_numeral(pow2 64);;
  val it : term = `18446744073709551616`

COMMENTS
The similar function mk_small_numeral works from a regular machine integer, Ocaml type int. If that suffices, it may be simpler.

SEE ALSO
dest_numeral, dest_small_numeral, is_numeral, mk_small_numeral, term_of_rat.