1\DOC dest_cons 2 3\TYPE {dest_cons : term -> term * term} 4 5\SYNOPSIS 6Breaks apart a `CONS pair' into head and tail. 7 8\DESCRIBE 9{dest_cons} is a term destructor for `CONS pairs'. When applied to a term 10representing a nonempty list {[t;t1;...;tn]} (which is equivalent to 11{CONS t [t1;...;tn]}), it returns the pair of terms 12{(t, [t1;...;tn])}. 13 14\FAILURE 15Fails if the term is an empty list. 16 17\SEEALSO 18listSyntax.mk_cons, listSyntax.is_cons, listSyntax.mk_list, listSyntax.dest_list, listSyntax.is_list. 19\ENDDOC 20