WORD_EVAL_CONV
wordsLib.WORD_EVAL_CONV : conv
Evaluation for words.
The conversion WORD_EVAL_CONV provides efficient evaluation for word
operations. It uses wordsLib.words_compset.
Example
> wordsLib.WORD_EVAL_CONV “word_log2 (word_reverse (3w * (33w #<< 4))) : word32”
val it = ⊢ word_log2 (word_reverse (3w * 33w ⇆ 4)) = 27w: thm
Comments
This conversion is best suited to evaluating ground terms with known
word lengths. The conversion wordsLib.WORD_CONV is a suitable
alternative.
See also
bossLib.EVAL,
computeLib.CBV_CONV,
wordsLib.WORD_LOGIC_CONV,
wordsLib.WORD_MUL_LSL_CONV,
wordsLib.WORD_CONV,
wordsLib.WORD_BIT_EQ_CONV,
wordsLib.WORD_EVAL_CONV