pairSyntax.dest

dest_prod : hol_type -> hol_type * hol_type

STRUCTURE: pairSyntax
LIBRARY: pair
SYNOPSIS: Breaks a product type into its two component types.
DESCRIPTION: dest_prod is a type destructor for products: dest_pair ":t1#t2" returns (":t1",":t2").
FAILURE: Fails with dest_prod if the argument is not a product type.
SEEALSO: is_prod, mk_prod

HOL Kananaskis-14