guess_lengths

wordsLib.guess_lengths : unit -> unit

Turns on word length guessing.

A call to guess_lengths adds a post-prcessing stage to the term parser: the function inst_word_lengths is used to instantiate type variables that are the return type of word_concat and word_extract.

Example

> show_types := true;
val it = (): unit

> val t1 = “(7 >< 5) a @@ (4 >< 0) a”;
val t1 =
   “(((((7 :num) >< (5 :num)) (a :δ word) :α word) @@
      (((4 :num) >< (0 :num)) a :β word))
       :γ word)”: term

> wordsLib.guess_lengths();
val it = (): unit

> val t2 = “(7 >< 5) a @@ (4 >< 0) a”;
val t2 =
   “(((((7 :num) >< (5 :num)) (a :δ word) :word3) @@
      (((4 :num) >< (0 :num)) a :word5))
       :word8)”: term
> type_of t2;
val it = “:word8”: hol_type

See also

wordsLib.inst_word_lengths, wordsLib.notify_on_word_length_guess