WORD_DIV_LSR_CONV : conv
STRUCTURE
wordsLib
DESCRIPTION
The conversion WORD_DIV_LSR_CONV replaces instances of unsigned division by a power of two with applications of logical right-shift.
EXAMPLE
> wordsLib.WORD_DIV_LSR_CONV ``w // 8w : word8``;
val it = |- w // 8w = w >>> 3: thm
COMMENTS
This conversion requires the word length to be known.
SEEALSO
WORD_MUL_LSL_CONV, WORD_MOD_BITS_CONV
HOL  Kananaskis-14