1\DOC LHS_CONV 2 3\TYPE {LHS_CONV : conv -> conv} 4 5\SYNOPSIS 6Applies a conversion to the left-hand argument of an equality. 7 8\KEYWORDS 9conversional 10 11\DESCRIBE 12If {c} is a conversion that maps a term {t1} to the theorem {|- t1 = t1'}, 13then the conversion {LHS_CONV c} maps applications of the form {t1 = t2} to 14theorems of the form: 15{ 16 |- (t1 = t2) = (t1' = t2) 17} 18 19 20\FAILURE 21{LHS_CONV c tm} fails if {tm} is not an an equality {t1 = t2}, 22or if {tm} has this form 23but the conversion {c} fails when applied to the term {t1}. The 24function returned by {LHS_CONV c} may also fail if the ML function 25{c:term->thm} is not, in fact, a conversion (i.e. a function that maps 26a term {t} to a theorem {|- t = t'}). 27 28\EXAMPLE 29{ 30- LHS_CONV REDUCE_CONV (Term`(3 + 5) = 7`); 31> val it = |- ((3 + 5) = 7) = (8 = 7) : thm 32} 33 34\COMMENTS 35{LAND_CONV} is similar, but works for any binary operator 36 37\SEEALSO 38Conv.BINOP_CONV, Conv.RHS_CONV, numLib.REDUCE_CONV, Conv.LAND_CONV. 39\ENDDOC 40