dest_cons : term -> term * term
STRUCTURE
SYNOPSIS
Breaks apart a ‘CONS pair’ into head and tail.
DESCRIPTION
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
HOL  Kananaskis-13