WORD_EVAL_CONV : conv
STRUCTURE
wordsLib
SYNOPSIS
Evaluation for words.
DESCRIPTION
The conversion WORD_EVAL_CONV provides efficient evaluation for word operations. It uses wordsLib.words_compset.
EXAMPLE
- 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.
SEEALSO
EVAL, CBV_CONV, WORD_LOGIC_CONV, WORD_MUL_LSL_CONV, WORD_CONV, WORD_BIT_EQ_CONV, WORD_EVAL_CONV
HOL  Kananaskis-13