diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-21 20:49:53 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-21 20:49:53 +0000 |
commit | 352d52ee7b5b854460361057c642ca1a5e00a7de (patch) | |
tree | ef8b111f5ef34155b25c70bfaad9dab87f4b6f7d | |
parent | c800ef013e87ada4f26246be4c8e8dd09f622afc (diff) |
Ajout projections; reparation script coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8440 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/RefMan-ext.tex | 96 |
1 files changed, 61 insertions, 35 deletions
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex index 87c8e3edb..5bb620459 100644 --- a/doc/RefMan-ext.tex +++ b/doc/RefMan-ext.tex @@ -112,22 +112,15 @@ Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. \end{coq_example*} \begin{coq_eval} -Lemma plus_m_n_eq_n_O : forall m n:nat, m + n = 0 -> n = 0. -destruct m; trivial. -intros; discriminate. -Qed. Lemma mult_m_n_eq_m_1 : forall m n:nat, m * n = 1 -> m = 1. destruct m; trivial. intros; apply f_equal with (f := S). -generalize H. -case n; trivial. -simpl. -case n0; simpl. -intro; rewrite <- mult_n_O; intro; discriminate. -intros n1 n2 H0; injection H0. -intro H1. -set (H2 := (plus_m_n_eq_n_O n1 (S (n1 + n2 * S n1)) H1)). -discriminate. +destruct m; trivial. +destruct n; simpl in H. + rewrite <- mult_n_O in H. + discriminate. + rewrite <- plus_n_Sm in H. + discriminate. Qed. intros x y z [H1 H2]. @@ -190,6 +183,38 @@ of the chapter devoted to coercions. \Rem {\tt Structure} is a synonym of the keyword {\tt Record}. +\Rem An experimental syntax for projections based on a dot notation is +available. The command to activate it is + +\bigskip +{\tt Set Printing Projections.} +\bigskip + +The corresponding grammar is: +\bigskip + +\begin{tabular}{|lcl|} +\hline +{\term} & ++= & {\term} {\tt .(} {\qualid} {\tt )}\\ + & $|$ & {\term} {\tt .(} {\qualid} \nelist{\termarg}{} {\tt )}\\ + & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )}\\ +\hline +\end{tabular} +\bigskip + +When {\qualid} denotes a projection, the syntax {\tt +{\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax {\tt +{\term}.({\qualid}~{\termarg}$_1$~ \ldots~ {\termarg}$_n$)} to +{\qualid~{\termarg}$_1$ \ldots {\termarg}$_n$~\term}, and the syntax +{\tt {\term}.(@{\qualid}~{\term}$_1$~\ldots~{\term}$_n$)} to +{@\qualid~{\term}$_1$ \ldots {\term}$_n$~\term}. In each case, {\term} +is the object projected and the other arguments are the parameters of +the inductive type. + +To deactivate the printing of projections, use +{\tt Unset Printing Projections}. + + \section{Variants and extensions of {\tt match}} \label{Extensions-of-match} \index{match@{\tt match\ldots with\ldots end}} @@ -456,32 +481,33 @@ Print fst. % ancestor of \texttt{match}. Again, it is still in the code for % compatibility with old versions but the user should not use it. -\section{Forced type} +% Explained in RefMan-gal.tex +%% \section{Forced type} -In some cases, one may wish to assign a particular type to a term. The -syntax to force the type of a term is the following: +%% In some cases, one may wish to assign a particular type to a term. The +%% syntax to force the type of a term is the following: -\medskip -\begin{tabular}{lcl} -{\term} & ++= & {\term} {\tt :} {\term}\\ -\end{tabular} -\medskip +%% \medskip +%% \begin{tabular}{lcl} +%% {\term} & ++= & {\term} {\tt :} {\term}\\ +%% \end{tabular} +%% \medskip -It forces the first term to be of type the second term. The -type must be compatible with -the term. More precisely it must be either a type convertible to -the automatically inferred type (see chapter \ref{Cic}) or a type -coercible to it, (see \ref{Coercions}). When the type of a -whole expression is forced, it is usually not necessary to give the types of -the variables involved in the term. +%% It forces the first term to be of type the second term. The +%% type must be compatible with +%% the term. More precisely it must be either a type convertible to +%% the automatically inferred type (see chapter \ref{Cic}) or a type +%% coercible to it, (see \ref{Coercions}). When the type of a +%% whole expression is forced, it is usually not necessary to give the types of +%% the variables involved in the term. -Example: +%% Example: -\begin{coq_example} -Definition ID := forall X:Set, X -> X. -Definition id := (fun X x => x):ID. -Check id. -\end{coq_example} +%% \begin{coq_example} +%% Definition ID := forall X:Set, X -> X. +%% Definition id := (fun X x => x):ID. +%% Check id. +%% \end{coq_example} \section{Section mechanism}\index{Sections}\label{Section} The sectioning mechanism allows to organise a proof in structured @@ -932,7 +958,7 @@ partial applications, the synthesis of implicit arguments may fail, so one may have to give explicitly certain implicit arguments of an application. The syntax for this is {\tt (\ident:=\term)} where {\ident} is the name of the implicit argument and {\term} is its corresponding -explicit term. Alternatively, one can locally desactivate the hidding of +explicit term. Alternatively, one can locally deactivate the hidding of implicit arguments of a function by using the notation {\tt @{\qualid}~{\term}$_1$..{\term}$_n$}. |