diff options
| -rw-r--r-- | doc/RefMan-gal.tex | 50 | ||||
| -rwxr-xr-x | doc/RefMan-syn.tex | 31 |
2 files changed, 58 insertions, 23 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index 5a4983151..8be425c13 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -381,7 +381,8 @@ subclass of the syntactic class {\term}. \index{specif@{\specif}} \item {\Type} is the type of {\Set} and {\Prop} \end{itemize} -More on sorts can be found in section \ref{Sorts}. +More on sorts can be found in section~\ref{Sorts}. +\noindent More on sorts can be found in section \ref{Sorts}. \subsection{Binders \label{Binders} @@ -737,7 +738,6 @@ environment}\index{Environment}. A formal presentation of constants and environments is given in Section~\ref{Typed-terms}. - \subsubsection{\tt Definition {\ident} := {\term}. \comindex{Definition}} @@ -770,22 +770,22 @@ environment, provided that {\term} is well-typed. \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold} -\subsubsection{\tt Local {\ident} := {\term}. -\comindex{Local}} +\subsubsection{\tt Let {\ident} := {\term}. +\comindex{Let}} This command binds the value {\term} to the name {\ident} in the -environment of the current section. The name {\ident} will be unknown -when the current section will be closed and all occurrences of -{\ident} in persistent objects (such as theorems) defined within the -section will be replaced by \term. One can say that the {\tt Local} -definition is a kind of {\em macro}. +environment of the current section. The name {\ident} disappears +when the current section is eventually closed, and, all +persistent objects (such as theorems) defined within the +section and depending on {\ident} are prefixed by the local definition +{\tt let {\ident} := {\term} in}. \begin{ErrMsgs} \item \errindex{Clash with previous constant {\ident}} \end{ErrMsgs} \begin{Variants} -\item {\tt Local {\ident} : {\term$_1$} := {\term$_2$}.} +\item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.} \end{Variants} \SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque}, @@ -831,7 +831,7 @@ for {\ident}. This condition ensures the soundness of the inductive definition. If this is the case, the constants {\ident}, {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with their respective types. Accordingly to the universe where -the inductive type lives({\it e.g.} its type {\sort}), {\Coq} provides a +the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a number of destructors for {\ident}. Destructors are named {\ident}{\tt\_ind}, {\ident}{\tt \_rec} or {\ident}{\tt \_rect} which respectively correspond to elimination principles on {\tt Prop}, {\tt @@ -919,10 +919,10 @@ induction principle we got for {\tt nat}. \begin{ErrMsgs} \item \errindex{Non strictly positive occurrence of {\ident} in {\type}} -\item \errindex{Type of Constructor not well-formed} +\item \errindex{The conclusion of {\type} is not valid; it must be +built from {\ident}} \end{ErrMsgs} - \subsubsection{Parameterized inductive types} Inductive types may be parameterized. Parameters differ from inductive @@ -939,21 +939,21 @@ The general scheme is: A typical example is the definition of polymorphic lists: \begin{coq_example*} -Inductive list (X:Set) : Set := - | Nil : list X - | Cons : X -> list X -> list X. +Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. \end{coq_example*} -Note that in the type of {\tt Nil} and {\tt Cons}, we write {\tt - (list X)} and not just {\tt list}.\\ The constants {\tt Nil} and -{\tt Cons} will have respectively types: +Note that in the type of {\tt nil} and {\tt cons}, we write {\tt + (list A)} and not just {\tt list}.\\ The constants {\tt nil} and +{\tt cons} will have respectively types: \begin{coq_example} -Check Nil. -Check Cons. +Check nil. +Check cons. \end{coq_example} -Types of destructors will be also quantified with {\tt (X:Set)}. +Types of destructors are also quantified with {\tt (A:Set)}. \begin{coq_eval} Reset Initial. @@ -961,12 +961,16 @@ Reset Initial. \begin{Variants} \item \begin{coq_example*} -Inductive list (X:Set) : Set := Nil | Cons (_:X) (_:list X). +Inductive list (A:Set) : Set := nil | cons (_:X) (_:list X). \end{coq_example*} This is an alternative definition of lists where we specify the arguments of the constructors rather than their full type. \end{Variants} +\begin{ErrMsgs} +\item \errindex{The {\num}th argument of {\ident} must be {\ident'} in {\type}} +\end{ErrMsgs} + \SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{elim}. diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex index 12ca5fc10..c948f25f8 100755 --- a/doc/RefMan-syn.tex +++ b/doc/RefMan-syn.tex @@ -135,16 +135,46 @@ Notation "x = y" := (@eq ? x y) (at level 70, no associativity). One can define {\em closed} notations whose both sides are symbols. In this case, the default precedence level for inner subexpression is 200. +\begin{coq_eval} +Set Printing Depth 50. +(********** The following is correct but produces **********) +(**** an incompatibility with the reserved notation ********) +\end{coq_eval} \begin{coq_example*} Notation "{ A } + { B }" := (sumbool A B) (at level 0). \end{coq_example*} One can also define notations for binders. +\begin{coq_eval} +Set Printing Depth 50. +(********** The following is correct but produces **********) +(**** an incompatibility with the reserved notation ********) +\end{coq_eval} \begin{coq_example*} Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0). \end{coq_example*} +In the last case though, there is a conflict with the notation for +type casts. This notation, as shown by the command {\tt Print Grammar +constr} is at level 100. To avoid $x:A$ being parsed at a type cast, +it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a +correct definition is + +\begin{coq_example*} +Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99). +\end{coq_example*} + +This change has retrospectively an effect on the notation for notation +{\tt "{ A } + { B }"}. For the sake of factorisation, {\tt A} must be +put at level 99 too, which gives + +\begin{coq_example*} +Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99). +\end{coq_example*} + +See the next section for more about factorisation. + \subsection{Simple factorisation rules} {\Coq} extensible parsing is performed by Camlp4 which is essentially a @@ -527,6 +557,7 @@ interpreted in the scope stack extended with the scope bound to {\nterm{key}}. To bind a delimiting key to a scope, use the command + \begin{quote} \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} \end{quote} |