\DOC dest_cons

\TYPE {dest_cons : term -> term * term}

\SYNOPSIS
Breaks apart a `CONS pair' into head and tail.

\DESCRIBE
{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.

\SEEALSO
listSyntax.mk_cons, listSyntax.is_cons, listSyntax.mk_list, listSyntax.dest_list, listSyntax.is_list.
\ENDDOC