mk_realintconst : num -> term

SYNOPSIS
Converts an OCaml number to a canonical integer literal of type :real.

DESCRIPTION
The call mk_realintconst n where n is an OCaml number (type num) produces the canonical literal of type :real representing the integer n. This will be of the form `&m' for a numeral m (when n is nonnegative) or `-- &m' for a nonzero numeral m (when n is negative).

FAILURE CONDITIONS
Fails if applied to a number that is not an integer (type num also includes rational numbers).

EXAMPLE
  # mk_realintconst (Int (-101));;
  val it : term = `-- &101`

  # type_of it;;
  val it : hol_type = `:real`

SEE ALSO
dest_realintconst, is_realintconst, mk_intconst, rat_of_term.