The cross product operation is familiar from set theory and calculus (where it is called the {\em cartesian} product). The cross product type is, as we would expect, the type of pairs of elements from two other types. It is defined by:
In ML the cross product of A and B is written A #B. An element of such a product is written in ML as a, b. We say that , is the infix type constructor for pairs.
Equality on pairs is defined by:
Note that this is decidable as long as equality is decidable for the component types.