1\DOC BINOP_CONV
2
3\TYPE {BINOP_CONV : conv -> conv}
4
5\SYNOPSIS
6Applies a conversion to both arguments of a binary operator.
7
8\KEYWORDS
9conversional.
10
11\LIBRARY
12
13
14\DESCRIBE
15If {c} is a conversion that when applied to {t1} returns the theorem
16{|- t1 = t1'} and when applied to {t2} returns the theorem
17{|- t2 = t2'}, then {BINOP_CONV c (Term`f t1 t2`)} will return the
18theorem
19{
20   |- f t1 t2 = f t1' t2'
21}
22
23
24\FAILURE
25{BINOP_CONV c t} will fail if {t} is not of the general form
26{f t1 t2}, or if {c} fails when applied to either {t1} or {t2}, or if {c}
27fails to return theorems of the form {|- t1 = t1'} and {|- t2 = t2'}
28when applied to those arguments.  (The latter case would imply that
29{c} wasn't a conversion at all.)
30
31\EXAMPLE
32{
33- BINOP_CONV REDUCE_CONV (Term`3 * 4 + 6 * 7`);
34> val it = |- 3 * 4 + 6 * 7 = 12 + 42 : thm
35}
36
37
38\SEEALSO
39Conv.FORK_CONV, Conv.LAND_CONV, Conv.RAND_CONV, Conv.RATOR_CONV,
40numLib.REDUCE_CONV.
41\ENDDOC
42