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.