WORD_MOD_BITS_CONV
wordsLib.WORD_MOD_BITS_CONV : conv
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
Comments
This conversion requires the word length to be known.