dest_cons : term -> term * term
STRUCTURE
listSyntax
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
mk_cons
,
is_cons
,
mk_list
,
dest_list
,
is_list
HOL
Kananaskis-14