GEN_BETA_CONV : term -> thm

SYNOPSIS
Beta-reduces general beta-redexes (e.g. paired ones).

DESCRIPTION
The conversion GEN_BETA_CONV will perform beta-reduction of simple beta-redexes in the manner of BETA_CONV, or of generalized beta-redexes such as paired redexes.

FAILURE CONDITIONS
GEN_BETA_CONV tm fails if tm is neither a simple nor a tupled beta-redex.

EXAMPLE
The following examples show the action of GEN_BETA_CONV on tupled redexes and others:
  # GEN_BETA_CONV `(\x. x + 1) 2`;;
  val it : thm = |- (\x. x + 1) 2 = 2 + 1

  # GEN_BETA_CONV `(\(x,y,z). x + y + z) (1,2,3)`;;
  val it : thm = |- (\(x,y,z). x + y + z) (1,2,3) = 1 + 2 + 3

  # GEN_BETA_CONV `(\[a;b;c]. b) [1;2;3]`;;
  val it : thm = |- (\[a; b; c]. b) [1; 2; 3] = 2
However, it will fail if there is a mismatch between the varstruct and the argument, or if it is unable to make sense of the generalized abstraction:
  # GEN_BETA_CONV `(\(SUC n). n) 3`;;
  Exception: Failure "term_pmatch".

  # GEN_BETA_CONV `(\(x,y,z). x + y + z) (1,x)`;;
  Exception: Failure "dest_comb: not a combination".

SEE ALSO
BETA_CONV, MATCH_CONV.