inst_word_lengths
wordsLib.inst_word_lengths : term -> term
Guess and instantiate word index type variables in a term.
The function inst_word_lengths tries to instantiate type variables
that correspond with the return type of word_concat and
word_extract.
Example
> load "wordsLib";
val it = (): unit
> wordsLib.inst_word_lengths “(7 >< 5) a @@ (4 >< 0) a”;
val it = “(7 >< 5) a @@ (4 >< 0) a”: term
> type_of it;
val it = “:word8”: hol_type
Comments
The function guess_lengths adds inst_word_lengths as a
post-processing stage to the term parser.
See also
wordsLib.guess_lengths,
wordsLib.notify_on_word_length_guess