mk_small_numeral : int -> term
- SYNOPSIS
-
Maps a nonnegative integer to corresponding numeral term.
- DESCRIPTION
-
The call mk_small_numeral n where n is a nonnegative OCaml machine integer
returns the HOL numeral representation of n.
- FAILURE CONDITIONS
-
Fails if the argument is negative.
- EXAMPLE
-
# mk_small_numeral 12;;
val it : term = `12`
- COMMENTS
-
The similar function mk_numeral works from an unlimited precision integer,
OCaml type num. However, none of HOL's inference rules depend on the
behaviour of machine integers, so logical soundness is not an issue.
- SEE ALSO
-
dest_numeral, dest_small_numeral, is_numeral, mk_numeral, term_of_rat.