Clarify Cartesian-product operator

This commit is contained in:
Adam Chlipala 2020-01-08 14:36:27 -05:00
parent 93ef5add7a
commit 958906a2e5

View file

@ -217,6 +217,8 @@ Such types can be defined by enumerating their \emph{constructor}\index{construc
\mathsf{Times} &:& \mathsf{Exp} \times \mathsf{Exp} \to \mathsf{Exp}
\end{eqnarray*}
Note that the ``$\times$'' here is not the multiplication operator of concrete syntax, but rather the Cartesian-product operator\index{Cartesian product} of set theory, to indicate a type of pairs!
Such a list of constructors defines the set $\mathsf{Exp}$ to contain exactly those terms that can be built up with the constructors.
In inference-rule notation:
\encoding