Changeset 2521 for Papers


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

..

File:
1 edited

Legend:

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

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