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