RHS_CONV
Conv.RHS_CONV : conv -> conv
Applies a conversion to the right-hand argument of an equality.
If c is a conversion that maps a term t2 to the theorem
|- t2 = t2', then the conversion RHS_CONV c maps applications of the
form t1 = t2 to theorems of the form:
|- (t1 = t2) = (t1 = t2')
Failure
RHS_CONV c tm fails if tm is not an an equality t1 = t2, or if
tm has this form but the conversion c fails when applied to the term
t2. The function returned by RHS_CONV c may also fail if the ML
function c:term->thm is not, in fact, a conversion (i.e. a function
that maps a term t to a theorem |- t = t').
Example
> RHS_CONV reduceLib.REDUCE_CONV (Term`7 = (3 + 5)`);
val it = ⊢ 7 = 3 + 5 ⇔ 7 = 8: thm
Comments
RAND_CONV is similar, but works for any binary operator
See also
Conv.BINOP_CONV,
Conv.LHS_CONV,
numLib.REDUCE_CONV,
Conv.RAND_CONV