mk_word_size
wordsLib.mk_word_size : int -> unit
Adds a type abbreviation and theorems for a given word length.
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
> wordsLib.mk_word_size 128
val it = (): unit
> “:word128”
val it = “:word128”: 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.