dest_list : term -> term list * hol_type
STRUCTURE
listSyntax
SYNOPSIS
Iteratively breaks apart a list term.
DESCRIPTION
dest_list
is a term destructor for lists:
dest_list ``[t1;...;tn]:ty list``
returns
([t1,...,tn], ty)
.
FAILURE
Fails if the term is not a list.
SEEALSO
mk_list
,
is_list
,
mk_cons
,
dest_cons
,
is_cons
HOL
Kananaskis-13