# Changeset 2526 for Papers/polymorphic-variants-2012

Ignore:
Timestamp:
Dec 3, 2012, 5:48:57 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2525 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}