----------------------------------------------------------------------
dest_cons                                                 (listSyntax)
----------------------------------------------------------------------
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.

----------------------------------------------------------------------