Globals.show_types : bool ref
STRUCTURE
SYNOPSIS
Flag controlling printing of HOL types (in terms).
DESCRIPTION
Normally HOL types in terms are not printed, since this makes terms hard to read. Type printing is enabled by show_types := true, and disabled by show_types := false. When printing of types is enabled, not all variables and constants are annotated with a type. The intention is to provide sufficient type information to remove any ambiguities without swamping the term with type information.
FAILURE
Never fails.
EXAMPLE
- BOOL_CASES_AX;;
> val it = |- !t. (t = T) \/ (t = F) : thm

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

- BOOL_CASES_AX;;
> val it = |- !(t :bool). (t = T) \/ (t = F) : thm

COMMENTS
It is possible to construct an abstraction in which the bound variable has the same name but a different type to a variable in the body. In such a case the two variables are considered to be distinct. Without type information such a term can be very misleading, so it might be a good idea to provide type information for the free variable whether or not printing of types is enabled.
SEEALSO
HOL  Trindemossen-1