RAND_CONV : conv -> conv

SYNOPSIS
Applies a conversion to the operand of an application.

DESCRIPTION
If c is a conversion that maps a term `t2` to the theorem |- t2 = t2', then the conversion RAND_CONV c maps applications of the form `t1 t2` to theorems of the form:
   |- (t1 t2) = (t1 t2')
That is, RAND_CONV c `t1 t2` applies c to the operand of the application `t1 t2`.

FAILURE CONDITIONS
RAND_CONV c tm fails if tm is not an application or if tm has the form `t1 t2` but the conversion c fails when applied to the term t2. The function returned by RAND_CONV c may also fail if the ML function c is not, in fact, a conversion (i.e. a function that maps a term t to a theorem |- t = t').

EXAMPLE
  # RAND_CONV num_CONV `SUC 2`;;
  val it : thm = |- SUC 2 = SUC (SUC 1)

SEE ALSO
ABS_CONV, COMB_CONV, COMB_CONV2, LAND_CONV, RATOR_CONV, SUB_CONV.