1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
\DOC dest_const
\TYPE {dest_const : term -> string * hol_type}
\SYNOPSIS
Breaks apart a constant into name and type.
\DESCRIBE
{dest_const} is a term destructor for constants:
{
dest_const `const:ty`
}
\noindent returns {("const",`:ty`)}.
\FAILURE
Fails with {dest_const} if term is not a constant.
\EXAMPLE
{
# dest_const `T`;;
val it : string * hol_type = ("T", `:bool`)
}
\SEEALSO
dest_abs, dest_comb, dest_var, is_const, mk_const, mk_mconst, name_of.
\ENDDOC
|
