bvar : term -> term
STRUCTURE
Term
SYNOPSIS
Returns the bound variable of an abstraction.
DESCRIPTION
If
M
is a lambda abstraction, i.e, has the form
\v. t
, then
bvar M
returns
v
.
FAILURE
Fails unless
M
is an abstraction.
SEEALSO
body
,
dest_abs
HOL
Kananaskis-14