----------------------------------------------------------------------
notify_on_word_length_guess                                 (wordsLib)
----------------------------------------------------------------------
notify_on_word_length_guess : bool ref

SYNOPSIS
Controls notification of word length guesses.

DESCRIBE
When the reference {notify_on_word_length_guess} is true a HOL message is
printed (in interactive sessions) when the function {inst_word_lengths}
instantiates types in a term.

EXAMPLE

- load "wordsLib";
...
- wordsLib.notify_on_word_length_guess := false;
> val it = () : unit
- wordsLib.inst_word_lengths ``(7 >< 5) a @@ (4 >< 0) a``;
<<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd>>
> val it = ``(7 >< 5) a @@ (4 >< 0) a`` : term
- type_of it;
> val it = ``:bool[8]`` : hol_type


COMMENTS
By default {notify_on_word_length_guess} is true.

SEEALSO
wordsLib.guess_lengths, wordsLib.inst_word_lengths.

----------------------------------------------------------------------