Globals.show_numeral_types : bool ref
STRUCTURE
SYNOPSIS
A flag which causes numerals to be printed with suffix annotation when true.
LIBRARY
Globals
DESCRIPTION
This flag controls the pretty-printing of numeral forms that have been added to the global grammar with the function add_numeral_form. If the flag is true, then all numeric values are printed with the single-letter suffixes that identify which type the value is.
FAILURE
Never fails, as it is just an SML value.
EXAMPLE
- load "integerTheory";
> val it = () : unit

- Term`~3`;
> val it = `~3` : term

- show_numeral_types := true;
> val it = () : unit

- Term`~3`;
> val it = `~3i` : term

USES
Can help to disambiguate terms involving numerals.
SEEALSO
HOL  Trindemossen-1