dest_strip_comb : term -> string * term list
STRUCTURE
SYNOPSIS
Strips a function application, and breaks head constant.
DESCRIPTION
If t is a term of the form c t1 t2 .. tn, with c a constant, then a call to dest_strip_comb t returns a pair (s,[t1,...,tn]), where s is a string of the form thy$name. The thy prefix identifies the theory where the constant was defined, and the name suffix is the constant’s name.
FAILURE
Fails if the term is not a constant applied to zero or more arguments.
EXAMPLE
> dest_strip_comb ``SUC 2``;
val it = ("num$SUC", [``2``]) : string * term list
COMMENTS
Useful for pattern-matching at the ML level, where doing a case on Lib.total dest_strip_comb t allows patterns of interest to be idiomatically identified. In the absence of view-patterns in SML, one has to use custom destructors.
SEEALSO
HOL  Kananaskis-14