1\DOC
2
3\TYPE {dest_strip_comb : term -> string * term list}
4
5\SYNOPSIS
6Strips a function application, and breaks head constant.
7
8\KEYWORDS
9
10\DESCRIBE
11If {t} is a term of the form {c t1 t2 .. tn}, with {c} a constant,
12then a call to {dest_strip_comb t} returns a pair {(s,[t1,...,tn])},
13where {s} is a string of the form {thy$name}. The {thy} prefix
14identifies the theory where the constant was defined, and the {name}
15suffix is the constant���s name.
16
17\FAILURE
18Fails if the term is not a constant applied to zero or more arguments.
19
20\EXAMPLE
21{
22> dest_strip_comb ``SUC 2``;
23val it = ("num$SUC", [``2``]) : string * term list
24}
25
26\COMMENTS
27Useful for pattern-matching at the ML level, where doing a {case} on
28{Lib.total dest_strip_comb t} allows patterns of interest to be
29idiomatically identified. In the absence of view-patterns in SML, one
30has to use custom destructors.
31
32\SEEALSO
33HolKernel.dest_term.
34
35\ENDDOC
36