mk_list : {els : term list, ty : hol_type} -> term
STRUCTURE
listSyntax
SYNOPSIS
Constructs an object-level (HOL) list from an ML list of terms.
DESCRIPTION
mk_list{els = [t1, ..., tn], ty = ty}
returns
[t1;...;tn]:ty list
. The type argument is required so that empty lists can be constructed.
FAILURE
Fails if any term in the list is not of the type specified as the second argument.
SEEALSO
dest_list
,
is_list
,
mk_cons
,
dest_cons
,
is_cons
HOL
Kananaskis-10