WORD_BIT_EQ_CONV : conv
STRUCTURE
wordsLib
SYNOPSIS
Conversion based on WORD_BIT_EQ_ss.
DESCRIPTION
The conversion WORD_BIT_EQ_CONV performs simplification using fcpLib.FCP_ss.
EXAMPLE
- WORD_BIT_EQ_CONV ``a << 2 >>> 1 = ((5 -- 0) a << 1) :word8``
> val it = |- (a << 2 >>> 1 = (5 -- 0) a << 1) = T : thm
SEEALSO
WORD_BIT_EQ_ss, BBLAST_CONV, WORD_ARITH_CONV, WORD_LOGIC_CONV, WORD_MUL_LSL_CONV, WORD_CONV, WORD_EVAL_CONV
HOL  Trindemossen-1