dest_const : term -> string * hol_type
STRUCTURE
Term
SYNOPSIS
Breaks apart a constant into name and type.
DESCRIPTION
dest_const
is a term destructor for constants. If
M
is a constant with name
c
and type
ty
, then
dest_const M
returns
(c,ty)
.
FAILURE
Fails if
M
is not a constant.
COMMENTS
In Hol98, constants also carry the theory they are declared in. A more precise and robust way to analyze a constant is with
dest_thy_const
.
SEEALSO
mk_const
,
mk_thy_const
,
dest_thy_const
,
is_const
,
dest_abs
,
dest_comb
,
dest_var
HOL
Kananaskis-14