Beta

Thm.Beta : thm -> thm

Perform one step of beta-reduction on the right hand side of an equational theorem.

Beta performs a single beta-reduction step on the right-hand side of an equational theorem.

   A |- t = ((\x.M) N)
  --------------------- Beta
   A |- t = M [N/x]

Failure

If the theorem is not an equation, or if the right hand side of the equation is not a beta-redex.

Example

> val th = REFL “(K:'a ->'b->'a) x”;
val th = ⊢ K x = K x: thm

> SUBS_OCCS [([2],combinTheory.K_DEF)] th;
val it = ⊢ K x = (λx y. x) x: thm

> Beta it;
val it = ⊢ K x = (λy. x): thm

Comments

Beta is equivalent to RIGHT_BETA but faster.

See also

Drule.RIGHT_BETA, Drule.ETA_CONV