 Timestamp:
 Oct 25, 2012, 12:30:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2414 r2416 94 94 \begin{minipage}[b]{0.45\linewidth} 95 95 \begin{lstlisting} 96 96 97 \end{lstlisting} 97 98 \end{minipage} … … 123 124 \subsection{Matita} 124 125 \label{subsect.matita} 126 127 Matita~\cite{asperti:user:2007} is a dependentlytyped proof assistant developed in Bologna, implementing the Calculus of (Co)inductive Constructions, a type theory similar to that of Coq. 128 Throughout this paper, all running examples are provided in Matita's proof script vernacular. 129 This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward. 130 131 One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively. 132 Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. 133 134 Matita 125 135 126 136 \subsection{Subtyping as instantiation vs subtyping as safe static cast}
Note: See TracChangeset
for help on using the changeset viewer.