mk_numeral : Arbnum.num -> term
STRUCTURE
numSyntax
SYNOPSIS
Convert ML bignum value to HOL numeral.
DESCRIPTION
An invocation mk_numeral n, where n is an ML value of type Arbnum.num returns the corrresponding HOL term.
EXAMPLE
- Arbnum.fromString "1234";
> val it = 1234 : num

- mk_numeral it;
> val it = ``1234`` : term
FAILURE
Never fails.
SEEALSO
dest_numeral, is_numeral
HOL  Kananaskis-13