1\DOC
2
3\TYPE {mk_word_size : int -> unit}
4
5\SYNOPSIS
6
7Adds a type abbreviation and theorems for a given word length.
8
9\DESCRIBE
10
11An invocation of {mk_word_size n} introduces a type abbreviation for words of
12length {n}.  Theorems for {dimindex(:n)}, {dimword(:n)} and {INT_MIN(:n)} are
13generated and stored.
14
15\EXAMPLE
16{
17- mk_word_size 128
18> val it = () : unit
19- ``:word128``
20> val it = ``:bool[128]`` : hol_type
21- theorem "dimword_128"
22> val it = |- dimword (:128) = 340282366920938463463374607431768211456 : thm
23}
24
25\COMMENTS
26
27The type abbreviation will only print when {type_pp.pp_array_types} is set to
28{false}.
29
30\SEEALSO
31
32Parse.type_abbrev, wordsLib.SIZES_CONV, wordsLib.SIZES_ss
33
34\ENDDOC
35