# Changeset 2521 for Papers/polymorphic-variants-2012/polymorphic-variants.tex

Ignore:
Timestamp:
Dec 3, 2012, 4:10:22 PM (8 years ago)
Message:

..

File:
1 edited

Unmodified
Added
Removed
• ## Papers/polymorphic-variants-2012/polymorphic-variants.tex

 r2519 \item Its shallow encoding, the corresponding inductive type $$inductive~u~(\alpha_1:Type,\ldots,\alpha_m:Type) u : Type := K_1:T_1 \to u~\alpha_1~\ldots~\alpha_m ~|~ \ldots ~|~ K_n:T_n \to u~\alpha_1~\ldots~\alpha_m$$ K_1:T_1 \to u~\alpha_1~\ldots~\alpha_m ~|~ \ldots ~|~ K_n:T_n \to u~\alpha_1~\ldots~\alpha_m$$\item A disjoint sum (an inductive type) of names for the tags of u:$$inductive~tag_~ : Type := k_1: tag_ ~|~ \ldots ~|~ k_n: tag_$$\item An equality test eq_tag: tag_ \to tag_ \to bool that returns true$$inductive~tag\_~ : Type := k_1: tag\_ ~|~ \ldots ~|~ k_n: tag\_$$\item An equality test eq\_tag: tag\_ \to tag\_ \to bool that returns true iff the two tags are the same. This is boilerplate code that is often automatized by interactive theorem provers. We write tag for the type the tag_ coupled with its decidable equality test eq_tag. This is just the tag\_ coupled with its decidable equality test eq\_tag. This is just a minor technicality of no importance. \item A simple function$$tag_of_expr: \forall \alpha_1,\ldots,\alpha_m. \item A simple function $$tag\_of\_expr: \forall \alpha_1,\ldots,\alpha_m. u \alpha_1 \ldots \alpha_m \to tag$$ that performs a case analysis on the shallow encoding of a universe \end{lstlisting} Here, \texttt{mk\_DeqSet} is the constructor of the \texttt{DeqSet} record. By convention in Matita, for a record type name \texttt{Foo}, there exists a constructor for that record type name \textt{mk\_Foo}. By convention in Matita, for a record type name \texttt{Foo}, there exists a constructor for that record type name \texttt{mk\_Foo}. We pass the constructor function three arguments: the type that possess a decidable equality, in this case \texttt{tag\_}
Note: See TracChangeset for help on using the changeset viewer.