- Timestamp:
- Dec 3, 2012, 4:41:06 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/polymorphic-variants.tex
r2523 r2524 336 336 Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. 337 337 338 \subsection{Subtyping as instantiation vs subtyping assafe static cast}338 \subsection{Subtyping as instantiation \emph{vs} subtyping as a safe static cast} 339 339 340 340 \subsection{Syntax and type checking rules} … … 628 628 On the \texttt{tag\_} inductive type, we define the `obvious' decidable equality function: 629 629 \begin{lstlisting} 630 definition eq_tag \_: tag_ $\rightarrow$ tag_ $\rightarrow$ bool :=630 definition eq_tag_: tag_ $\rightarrow$ tag_ $\rightarrow$ bool := 631 631 $\lambda$t1, t2. 632 632 match t1 with
Note: See TracChangeset
for help on using the changeset viewer.