BETA_CONV : conv
STRUCTURE
SYNOPSIS
Performs a single step of beta-conversion.
DESCRIPTION
The conversion BETA_CONV maps a beta-redex "(\x.u)v" to the theorem
   |- (\x.u)v = u[v/x]
where u[v/x] denotes the result of substituting v for all free occurrences of x in u, after renaming sufficient bound variables to avoid variable capture. This conversion is one of the primitive inference rules of the HOL system.
FAILURE
BETA_CONV tm fails if tm is not a beta-redex.
EXAMPLE
- BETA_CONV (Term `(\x.x+1)y`);
> val it = |- (\x. x + 1)y = y + 1 :thm

- BETA_CONV (Term `(\x y. x+y)y`);
> val it = |- (\x y. x + y)y = (\y'. y + y') : thm

SEEALSO
HOL  Kananaskis-14