Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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