BETA_CONV : term -> thm

SYNOPSIS
Performs a simple 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 CONDITIONS
BETA_CONV tm fails if tm is not a beta-redex.

EXAMPLE
  # BETA_CONV `(\x. x + 1) y`;;
  val it : thm = |- (\x. x + 1) y = y + 1

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

COMMENTS
The HOL Light primitive rule BETA is the special case where the argument is the same as the bound variable. If you know that you are in this case, BETA is significantly more efficient. Though traditionally a primitive, BETA_CONV is actually a derived rule in HOL Light.

SEE ALSO
BETA, BETA_RULE, BETA_TAC, GEN_BETA_CONV, MATCH_CONV.