Amelioration explication syntaxe let et if

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8530 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 37 insertions, 3 deletions

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index ceacb3920..c9bcd3b38 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -236,9 +236,10 @@ its expanded form.
 \subsection{Pattern-matching on boolean values: the {\tt if} expression
 \index{if@{\tt if ... then ... else}}}
 
-For inductive types with exactly two constructors, it is possible to
-use a {\tt if ... then ... else} notation. For instance, the
-definition
+For inductive types with exactly two constructors and for
+pattern-matchings expressions which do not depend on the arguments of
+the constructors, it is possible to use a {\tt if ... then ... else}
+notation. For instance, the definition
 
 \begin{coq_example}
 Definition not (b:bool) :=
@@ -257,6 +258,32 @@ Reset not.
 Definition not (b:bool) := if b then false else true.
 \end{coq_example}
 
+More generally, for an inductive type with constructors {\tt C$_1$}
+and {\tt C$_2$}, we have the following equivalence
+
+\smallskip
+
+{\tt if {\term} \zeroone{\ifitem} then {\term}$_1$ else {\term}$_2$} $\equiv$
+\begin{tabular}[c]{l}
+{\tt match {\term} \zeroone{\ifitem} with}\\
+{\tt \verb!|! C$_1$ \_ {\ldots} \_ \verb!=>! {\term}$_1$} \\
+{\tt \verb!|! C$_2$ \_ {\ldots} \_ \verb!=>! {\term}$_2$} \\
+{\tt end}
+\end{tabular}
+
+Here is an example.
+
+\begin{coq_example}
+Check (fun x (H:{x=0}+{x<>0}) =>
+  match H with
+  | left _ => true
+  | right _ => false
+  end).
+\end{coq_example}
+
+Notice that the printing uses the {\tt if} syntax because {\tt sumbool} is
+declared as such (see section \ref{printing-options}).
+
 \subsection{Irrefutable patterns: the destructuring {\tt let}
 \index{let in@{\tt let ... in}}
 \label{Letin}}
@@ -296,6 +323,13 @@ The pretty-printing of a definition by matching on a
 irrefutable pattern can either be done using {\tt match} or the {\tt
 let} construction (see Section~\ref{printing-options}).
 
+The general equivalence for an inductive type with one constructors {\tt C} is
+
+\smallskip
+{\tt let ({\ident}$_1$,\ldots,{\ident}$_n$) \zeroone{\ifitem} := {\term} in {\term}'} \\
+$\equiv\;$
+{\tt match {\term} \zeroone{\ifitem} with \verb!|! C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
+
 \subsection{Options for pretty-printing of {\tt match}
 \label{printing-options}}