WORD_MUL_LSL_CONV : conv
STRUCTURE
wordsLib
SYNOPSIS
Conversion based on WORD_MUL_LSL_ss.
DESCRIPTION
The conversion WORD_MUL_LSL_CONV converts a multiplication by a word literal into a sum of left shifts.
EXAMPLE
- WORD_MUL_LSL_CONV ``49w * a``
> val it = |- 49w * a = a << 5 + a << 4 + a : thm
SEEALSO
WORD_MUL_LSL_ss, WORD_DIV_LSR_CONV, WORD_ARITH_CONV, WORD_LOGIC_CONV, WORD_CONV, WORD_BIT_EQ_CONV, WORD_EVAL_CONV
HOL  Kananaskis-13