dest_comb : term -> term * term
STRUCTURE
Term
SYNOPSIS
Breaks apart a combination (function application) into rator and rand.
DESCRIPTION
dest_comb
is a term destructor for combinations. If term
M
has the form
f x
, then
dest_comb M
equals
(f,x)
.
FAILURE
Fails if the argument is not a function application.
SEEALSO
mk_comb
,
is_comb
,
dest_var
,
dest_const
,
dest_abs
,
strip_comb
HOL
Kananaskis-13