BETAS_CONV : conv

SYNOPSIS

Beta conversion over multiple arguments.

DESCRIPTION

Given a term t of the form `(\x1 ... xn. t[x1,...,xn]) s1 ... sn`, the call BETAS_CONV t returns

  |- (\x1 ... xn. t[x1,...,xn]) s1 ... sn = t[s1,...,sn]

FAILURE CONDITIONS

Fails if the term is not of the form shown, for some n.

EXAMPLE

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

SEE ALSO

BETA_CONV, RIGHT_BETAS.