WORD_MOD_BITS_CONV : conv
STRUCTURE
DESCRIPTION
The conversion WORD_MOD_BITS_CONV replaces instances of word_mod by a power of two with applications of word_bits.
EXAMPLE
> wordsLib.WORD_MOD_BITS_CONV ``word_mod w 8w : word16``;
val it = |- word_mod w 8w = (2 -- 0) w: thm

wordsLib.WORD_MOD_BITS_CONV ``word_mod w 1w : word16``;
val it = |- word_mod w 1w = 0w: thm
COMMENTS
This conversion requires the word length to be known.
SEEALSO
HOL  Kananaskis-13