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