dest_cons
listSyntax.dest_cons : term -> term * term
Breaks apart a 'CONS pair' into head and tail.
dest_cons is a term destructor for 'CONS pairs'. When applied to a
term representing a nonempty list [t;t1;...;tn] (which is equivalent
to CONS t [t1;...;tn]), it returns the pair of terms
(t, [t1;...;tn]).
Failure
Fails if the term is an empty list.
See also
listSyntax.mk_cons,
listSyntax.is_cons,
listSyntax.mk_list,
listSyntax.dest_list,
listSyntax.is_list