notify_on_word_length_guess : bool ref
STRUCTURE
wordsLib
SYNOPSIS
Controls notification of word length guesses.
DESCRIPTION
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
guess_lengths, inst_word_lengths
HOL  Kananaskis-14