Index: /Papers/polymorphic-variants-2012/polymorphic-variants.tex
===================================================================
--- /Papers/polymorphic-variants-2012/polymorphic-variants.tex (revision 2525)
+++ /Papers/polymorphic-variants-2012/polymorphic-variants.tex (revision 2526)
@@ -674,4 +674,19 @@
satisfying requirement 1.
+\begin{definition}[Pattern matching encoding]
+A pattern match $match~t~with \{K_{n_j} \Rightarrow M_{n_j}\}^r_1$ that only considers a superset of the constructors listed in the polymorphic variant type
+$i$ is encoded as
+$match~t~with \{K_i \Rightarrow k_i \in i \to M'_i\}$
+where $M'_{n_j} = M_{n_j}$ for all $j \in [1,\ldots,r]$ and
+$M'_{n_j}$ is obtained by elimination of $False$ in all other cases.
+The proofs of $False$ required to perform the elimination are obtained from
+the hypotheses $k_i \in i$ which contradicts the fact that $k_i$ was not
+listed in a superset of $i$.
+\end{definition}
+Again, for closed types $i$, the test $k_i \in i$ can be implemented in such
+a way that it reduces to $False$ in all cases where a proof of $False$ is
+required. In the remaining case proof automation can be used to automatically
+find the proofs of absurdity.
+
\subsection{Simulation (reduction + type checking)}
\subsection{Examples}