dest_list

listSyntax.dest_list : term -> term list * hol_type

Iteratively breaks apart a list term.

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.

See also

listSyntax.mk_list, listSyntax.is_list, listSyntax.mk_cons, listSyntax.dest_cons, listSyntax.is_cons