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