----------------------------------------------------------------------
BINOP_CONV                                                      (Conv)
----------------------------------------------------------------------
BINOP_CONV : conv -> conv

SYNOPSIS
Applies a conversion to both arguments of a binary operator.

KEYWORDS
conversional.

LIBRARY


DESCRIBE
If {c} is a conversion that when applied to {t1} returns the theorem
{|- t1 = t1'} and when applied to {t2} returns the theorem
{|- t2 = t2'}, then {BINOP_CONV c (Term`f t1 t2`)} will return the
theorem

   |- f t1 t2 = f t1' t2'




FAILURE
{BINOP_CONV c t} will fail if {t} is not of the general form
{f t1 t2}, or if {c} fails when applied to either {t1} or {t2}, or if {c}
fails to return theorems of the form {|- t1 = t1'} and {|- t2 = t2'}
when applied to those arguments.  (The latter case would imply that
{c} wasn’t a conversion at all.)

EXAMPLE

- BINOP_CONV REDUCE_CONV (Term`3 * 4 + 6 * 7`);
> val it = |- 3 * 4 + 6 * 7 = 12 + 42 : thm




SEEALSO
Conv.FORK_CONV, Conv.LAND_CONV, Conv.RAND_CONV, Conv.RATOR_CONV,
numLib.REDUCE_CONV.

----------------------------------------------------------------------