EXPAND_REDUCE_CONV
wordsLib.EXPAND_REDUCE_CONV : conv
The conversion EXPAND_REDUCE_CONV expands out applications of
reduce_and, reduce_or, reduce_xor, reduce_nand, reduce_nor and
reduce_xnor.
Example
> wordsLib.EXPAND_REDUCE_CONV “reduce_and (w: word4)”;
val it =
⊢ reduce_and w = (((3 >< 3) w && (2 >< 2) w) && (1 >< 1) w) && (0 >< 0) w:
thm