dest_var : term -> string * hol_type
STRUCTURE
Term
SYNOPSIS
Breaks apart a variable into name and type.
DESCRIPTION
If
M
is a HOL variable, then
dest_var M
returns
(v,ty)
, where
v
is the name of the variable, an
ty
is its type.
FAILURE
Fails if
M
is not a variable.
SEEALSO
mk_var
,
is_var
,
dest_const
,
dest_comb
,
dest_abs
HOL
Kananaskis-14