1\DOC RED_CONV 2 3\TYPE {RED_CONV : conv} 4 5\SYNOPSIS 6Performs arithmetic or boolean reduction at top level if possible. 7 8\LIBRARY reduce 9 10\DESCRIBE 11The conversion {RED_CONV} attempts to apply, at the top level only, one 12of the following conversions from the {reduce} library (only one can succeed): 13{ 14 ADD_CONV AND_CONV BEQ_CONV COND_CONV 15 DIV_CONV EXP_CONV GE_CONV GT_CONV 16 IMP_CONV LE_CONV LT_CONV MOD_CONV 17 MUL_CONV NEQ_CONV NOT_CONV OR_CONV 18 PRE_CONV SBC_CONV SUC_CONV 19} 20 21\FAILURE 22Fails if none of the above conversions are applicable at top level. 23 24\EXAMPLE 25{ 26#RED_CONV "(2=3) = F";; 27|- ((2 = 3) = F) = ~(2 = 3) 28 29#RED_CONV "15 DIV 13";; 30|- 15 DIV 13 = 1 31 32#RED_CONV "100 + 100";; 33|- 100 + 100 = 200 34 35#RED_CONV "0 + x";; 36evaluation failed RED_CONV 37} 38 39\SEEALSO 40reduceLib.REDUCE_CONV, reduceLib.REDUCE_RULE, reduceLib.REDUCE_TAC 41 42\ENDDOC 43