mk_prod : hol_type * hol_type -> hol_type
STRUCTURE
pairSyntax
LIBRARY
pair
SYNOPSIS
Constructs a product type from two constituent types.
DESCRIPTION
mk_prod(ty1, ty2)
returns
ty1 # t2
.
FAILURE
Never fails.
SEEALSO
is_prod
,
dest_prod
HOL
Kananaskis-14