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