----------------------------------------------------------------------
beta_conv                                                       (Term)
----------------------------------------------------------------------
beta_conv : term -> term

SYNOPSIS
Performs one step of beta-reduction.

KEYWORDS
conversion, beta.

DESCRIBE
Beta-reduction is one of the primitive operations in the lambda calculus.
A step of beta-reduction may be performed by {beta_conv M}, where {M}
is the application of a lambda abstraction to an argument, i.e., has
the form {((\v.N) P)}. The beta-reduction occurs by systematically
replacing every free occurrence of {v} in {N} by {P}.

Care is taken so that no free variable of {P} becomes captured in
this process.

FAILURE
If {M} is not the application of an abstraction to an argument.

EXAMPLE

- beta_conv (mk_comb (Term `\(x:'a) (y:'b). x`, Term `(P:bool -> 'a) Q`));
> val it = `\y. P Q` : term

- beta_conv (mk_comb (Term `\(x:'a) (y:'b) (y':'b). x`, Term `y:'a`));
> val it = `\y'. y` : term




COMMENTS
More complex strategies for coding up full beta-reduction can be
coded up in ML. The {conversions} of Larry Paulson support this
activity as inference steps.

USES
For programming derived rules of inference.

SEEALSO
Thm.BETA_CONV, Drule.RIGHT_BETA, Drule.LIST_BETA_CONV,
Drule.RIGHT_LIST_BETA, Conv.DEPTH_CONV, Conv.TOP_DEPTH_CONV,
Conv.REDEPTH_CONV.

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