dest_abs : term -> term * term
STRUCTURE
Term
SYNOPSIS
Breaks apart an abstraction into abstracted variable and body.
DESCRIPTION
dest_abs
is a term destructor for abstractions: if
M
is a term of the form
\v.t
, then
dest_abs M
returns
(v,t)
.
FAILURE
Fails if it is not given a lambda abstraction.
SEEALSO
mk_abs
,
is_abs
,
dest_var
,
dest_const
,
dest_comb
,
strip_abs
HOL
Kananaskis-14