FORK_CONV
Conv.FORK_CONV : (conv * conv) -> conv
Applies a pair of conversions to the arguments of a binary operator.
If the conversion c1 maps a term t1 to the theorem |- t1 = t1',
and the conversion c2 maps t2 to |- t2 = t2', then the conversion
FORK_CONV (c1,c2) maps terms of the form f t1 t2 to theorems of the
form |- f t1 t2 = f t1' t2'.
Failure
FORK_CONV (c1,c2) t will fail if t is not of the general form
f t1 t2, or if c1 fails when applied to t1, or if c2 fails when
applied to t2, or if c1 or c2 aren't really conversions, and
thereby fail to return appropriate equational theorems.
Example
> FORK_CONV (BETA_CONV,reduceLib.REDUCE_CONV) (Term`(\x. x + 1)y * (10 DIV 3)`);
val it = ⊢ (λx. x + 1) y * (10 DIV 3) = (y + 1) * 3: thm
See also
Conv.BINOP_CONV,
Conv.LAND_CONV,
Conv.RAND_CONV,
Conv.RATOR_CONV,
numLib.REDUCE_CONV