\DOC

\TYPE {mk_word_size : int -> unit}

\SYNOPSIS

Adds a type abbreviation and theorems for a given word length.

\DESCRIBE

An invocation of {mk_word_size n} introduces a type abbreviation for words of
length {n}.  Theorems for {dimindex(:n)}, {dimword(:n)} and {INT_MIN(:n)} are
generated and stored.

\EXAMPLE
{
- mk_word_size 128
> val it = () : unit
- ``:word128``
> val it = ``:bool[128]`` : hol_type
- theorem "dimword_128"
> val it = |- dimword (:128) = 340282366920938463463374607431768211456 : thm
}

\COMMENTS

The type abbreviation will only print when {type_pp.pp_array_types} is set to
{false}.

\SEEALSO

Parse.type_abbrev, wordsLib.SIZES_CONV, wordsLib.SIZES_ss

\ENDDOC