BETA_CONV

Thm.BETA_CONV : conv

Performs a single step of beta-conversion.

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

See also

Conv.BETA_RULE, Tactic.BETA_TAC, Drule.LIST_BETA_CONV, PairedLambda.PAIRED_BETA_CONV, Drule.RIGHT_BETA, Drule.RIGHT_LIST_BETA