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