----------------------------------------------------------------------
LHS_CONV                                                        (Conv)
----------------------------------------------------------------------
LHS_CONV : conv -> conv

SYNOPSIS
Applies a conversion to the left-hand argument of an equality.

KEYWORDS
conversional

DESCRIBE
If {c} is a conversion that maps a term {t1} to the theorem {|- t1 = t1'},
then the conversion {LHS_CONV c} maps applications of the form {t1 = t2} to
theorems of the form:

   |- (t1 = t2) = (t1' = t2)




FAILURE
{LHS_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 {t1}. The
function returned by {LHS_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

- LHS_CONV REDUCE_CONV (Term`(3 + 5) = 7`);
> val it = |- ((3 + 5) = 7) = (8 = 7) : thm


COMMENTS
{LAND_CONV} is similar, but works for any binary operator

SEEALSO
Conv.BINOP_CONV, Conv.RHS_CONV, numLib.REDUCE_CONV, Conv.LAND_CONV.

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