Ignore:
Timestamp:
Dec 3, 2012, 4:41:06 PM (7 years ago)
Author:
mulligan
Message:

Avoiding conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2523 r2524  
    336336Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.
    337337
    338 \subsection{Subtyping as instantiation vs subtyping as safe static cast}
     338\subsection{Subtyping as instantiation \emph{vs} subtyping as a safe static cast}
    339339
    340340\subsection{Syntax and type checking rules}
    … …  
    628628On the \texttt{tag\_} inductive type, we define the `obvious' decidable equality function:
    629629\begin{lstlisting}
    630 definition eq_tag\_: tag_ $\rightarrow$ tag_ $\rightarrow$ bool :=
     630definition eq_tag_: tag_ $\rightarrow$ tag_ $\rightarrow$ bool :=
    631631  $\lambda$t1, t2.
    632632    match t1 with
Note: See TracChangeset for help on using the changeset viewer.