mk_cons : {hd :term, tl :term} -> term
STRUCTURE
listSyntax
SYNOPSIS
Constructs a
CONS
pair.
DESCRIPTION
mk_cons{hd = t, tl = `[t1;...;tn]`}
returns
`[t;t1;...;tn]`
.
FAILURE
Fails if
tl
is not a list or if
hd
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-10