diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /doc/refman/Classes.tex | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'doc/refman/Classes.tex')
-rw-r--r-- | doc/refman/Classes.tex | 31 |
1 files changed, 13 insertions, 18 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index f427609f..20ff649a 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -10,7 +10,7 @@ \label{typeclasses} \begin{flushleft} - \em The status of Type Classes is experimental. + \em The status of Type Classes is (extremely) experimental. \end{flushleft} This chapter presents a quick reference of the commands related to type @@ -128,7 +128,9 @@ particular support for type classes: methods. In the example above, \texttt{A} and \texttt{eqa} should be set maximally implicit. \item They support implicit quantification on partialy applied type - classes. + classes (\S \ref{implicit-generalization}). + Any argument not given as part of a type class binder will be + automatically generalized. \item They also support implicit quantification on superclasses (\S \ref{classes:superclasses}) \end{itemize} @@ -141,19 +143,6 @@ Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). Here \texttt{A} is implicitly generalized, and the resulting function is equivalent to the one above. -The parsing of generalized type-class binders is different from regular -binders: -\begin{itemize} -\item Implicit arguments of the class type are ignored. -\item Superclasses arguments are automatically generalized. -\item Any remaining arguments not given as part of a type class binder - will be automatically generalized. In other words, the rightmost - parameters are automatically generalized if not mentionned. -\end{itemize} - -One can switch off this special treatment using the $!$ mark in front of -the class name (see example below). - \asection{Parameterized Instances} One can declare parameterized instances as in \Haskell simply by giving @@ -242,9 +231,9 @@ Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). \end{coq_example*} In some cases, to be able to specify sharing of structures, one may want to give -explicitly the superclasses. It is possible to do it directly in regular -generalized binders, and using the \texttt{!} modifier in class -binders. For example: +explicitly the superclasses. It is is possible to do it directly in regular +binders, and using the \texttt{!} modifier in class binders. For +example: \begin{coq_example*} Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). @@ -378,6 +367,12 @@ instances at the end of sections, or declaring structure projections as instances. This is almost equivalent to {\tt Hint Resolve {\ident} : typeclass\_instances}. +\begin{Variants} +\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$} + \comindex{Existing Instances} + With this command, several existing instances can be declared at once. +\end{Variants} + \subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}} \comindex{Context} \label{Context} |