diff --git a/frap_book.tex b/frap_book.tex index 081d499..02b0ab0 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -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