mk_cons : term * term -> term
STRUCTURE
listSyntax
SYNOPSIS
Constructs a
CONS
pair.
DESCRIPTION
mk_cons (``t``, ``[t1;...;tn]``)
returns
``[t;t1;...;tn]``
.
FAILURE
Fails if the second element is not a list or if the first element is not of the same type as the elements of the list.
SEEALSO
dest_cons
,
is_cons
,
mk_list
,
dest_list
,
is_list
HOL
Kananaskis-13