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