type_invention_warning : bool ref

SYNOPSIS

Determined if user is warned about invented type variables.

DESCRIPTION

If HOL Light is unable to assign specific types to a term entered in quotation, it will invent its own type variables to use in the most general type. The flag type_invention_warning determines whether the user is warned in such situations. The default is true, since this can often indicate a user error (e.g. the user forgot to define a constant before using it in a term or overlooked more general types than expected). To disable the warnings, set it to false, while to make the checking even more rigorous and treat it as an error, set type_invention_error to true.

FAILURE CONDITIONS

Not applicable.

EXAMPLE

When the following term is entered, HOL Light invents a type variable to use as the most general type:

  # let tm = `x IN s`;;
  Warning: inventing type variables
  val tm : term = `x IN s`

which are not particularly intuitive, as you can see:

  # map dest_var (frees tm);;
  val it : (string * hol_type) list =
    [("x", `:?47676`); ("s", `:?47676->bool`)]

You can avoid this by explicitly giving appropriate types or type variables yourself:

  # let tm = `(x:A) IN s`;;
  val tm : term = `x IN s`

But if you often want to let HOL Light invent types for itself without warning you, set

  # type_invention_warning := false;;
  val it : unit = ()

One reason why you might find the warning more irritating than helpful is if you are rewriting with ad-hoc set theory lemmas generated like this:

  # SET_RULE `x IN UNIONS (a INSERT t) <=> x IN UNIONS t \/ x IN a`;;