`let_CONV : term -> thm`

SYNOPSIS
Evaluates let-terms in the HOL logic.

DESCRIPTION
The conversion let_CONV implements evaluation of object-language let-terms. When applied to a let-term of the form:
```   let v1 = t1 and ... and vn = tn in t
```
where v1, ..., vn are variables, let_CONV proves and returns the theorem:
```   |- (let v1 = t1 and ... and vn = tn in t) = t[t1,...,tn/v1,...,vn]
```
where t[t1,...,tn/v1,...,vn] denotes the result of substituting ti for v1 in parallel in t, with automatic renaming of bound variables to prevent free variable capture. let_CONV also works on let-terms that bind terms built up from applications of inductive type constructors. For example, if is an arbitrarily-nested tuple of distinct variables v1, ..., vn and is a structurally similar tuple of values, that is equals [t1,...,tn/v1,...,vn] for some terms t1, ..., tn, then:
```   let_CONV `let  =  in t`
```
returns
```  |- (let  =  in t) = t[t1,...,tn/v1,...,vn]
```
That is, the term ti is substituted for the corresponding variable vi in t. This form of let-reduction also works with simultaneous binding of tuples using and.

FAILURE CONDITIONS
let_CONV tm fails if tm is not a reducible let-term of one of the forms specified above.

EXAMPLE
A simple example of the use of let_CONV to eliminate a single local variable is the following:
```  # let_CONV `let x = 1 in x+y`;;
val it : thm = |- (let x = 1 in x + y) = 1 + y
```
and an example showing a tupled binding is:
```  # let_CONV `let (x,y) = (1,2) in x+y`;;
val it : thm = |- (let x,y = 1,2 in x + y) = 1 + 2
```
Simultaneous introduction of two bindings is illustrated by:
```  # let_CONV `let x = 1 and y = 2 in x + y + z`;;
val it : thm = |- (let x = 1 and y = 2 in x + y + z) = 1 + 2 + z
```