diff options
Diffstat (limited to 'doc/refman/RefMan-syn.tex')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 406 |
1 files changed, 293 insertions, 113 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index eecb5ac7c..836753db1 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -3,25 +3,32 @@ In this chapter, we introduce advanced commands to modify the way {\Coq} parses and prints objects, i.e. the translations between the -concrete and internal representations of terms and commands. The main -commands are {\tt Notation} and {\tt Infix} which are described in -section \ref{Notation}. It also happens that the same symbolic -notation is expected in different contexts. To achieve this form of -overloading, {\Coq} offers a notion of interpretation scope. This is -described in Section~\ref{scopes}. - -\Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which -were present for a while in {\Coq} are no longer available from {\Coq} -version 8.0. The underlying AST structure is also no longer available. -The functionalities of the command {\tt Syntactic Definition} are -still available; see Section~\ref{Abbreviations}. +concrete and internal representations of terms and commands. + +The main commands to provide custom symbolic notations for terms are +{\tt Notation} and {\tt Infix}. They are described in Section +\ref{Notation}. There is also a variant of {\tt Notation} which does +not modify the parser. This provides with a form of abbreviation and +it is described in Section~\ref{Abbreviations}. It is sometimes +expected that the same symbolic notation has different meanings in +different contexts. To achieve this form of overloading, {\Coq} offers +a notion of interpretation scope. This is described in +Section~\ref{scopes}. + +The main command to provide custom notations for tactics is {\tt + Tactic Notation}. It is described in Section~\ref{Tactic-Notation}. + +% No need any more to remind this +%% \Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which +%% were present for a while in {\Coq} are no longer available from {\Coq} +%% version 8.0. The underlying AST structure is also no longer available. \section[Notations]{Notations\label{Notation} \comindex{Notation}} \subsection{Basic notations} -A {\em notation} is a symbolic abbreviation denoting some term +A {\em notation} is a symbolic expression denoting some term or term pattern. A typical notation is the use of the infix symbol \verb=/\= to denote @@ -37,7 +44,7 @@ string \verb="A /\ B"= (called a {\em notation}) tells how it is symbolically written. A notation is always surrounded by double quotes (except when the -abbreviation is a single identifier; see \ref{Abbreviations}). The +abbreviation has the form of an ordinary applicative expression; see \ref{Abbreviations}). The notation is composed of {\em tokens} separated by spaces. Identifiers in the string (such as \texttt{A} and \texttt{B}) are the {\em parameters} of the notation. They must occur at least once each in the @@ -61,7 +68,7 @@ syntactic expression (see \ref{ReservedNotation}), explicit precedences and associativity rules have to be given. \Rem The right-hand side of a notation is interpreted at the time the -notation is given. In particular, implicit arguments (see +notation is given. In particular, disambiguation of constants, implicit arguments (see Section~\ref{Implicit Arguments}), coercions (see Section~\ref{Coercions}), etc. are resolved at the time of the declaration of the notation. @@ -105,8 +112,8 @@ parentheses are mandatory (this is a ``no associativity'')\footnote{ which {\Coq} is built, namely {\camlpppp}, currently does not implement the no-associativity and replaces it by a left associativity; hence it is the same for {\Coq}: no-associativity is in fact left associativity}. -We don't know of a special convention of the associativity of -disjunction and conjunction, so let's apply for instance a right +We do not know of a special convention of the associativity of +disjunction and conjunction, so let us apply for instance a right associativity (which is the choice of {\Coq}). Precedence levels and associativity rules of notations have to be @@ -142,7 +149,8 @@ Notation "x = y" := (@eq _ x y) (at level 70, no associativity). \end{coq_example*} One can define {\em closed} notations whose both sides are symbols. In -this case, the default precedence level for inner subexpression is 200. +this case, the default precedence level for inner subexpression is +200, and the default level for the notation itself is 0. \begin{coq_eval} Set Printing Depth 50. @@ -150,7 +158,7 @@ Set Printing Depth 50. (**** an incompatibility with the reserved notation ********) \end{coq_eval} \begin{coq_example*} -Notation "( x , y )" := (@pair _ _ x y) (at level 0). +Notation "( x , y )" := (@pair _ _ x y). \end{coq_example*} One can also define notations for binders. @@ -161,17 +169,17 @@ Set Printing Depth 50. (**** an incompatibility with the reserved notation ********) \end{coq_eval} \begin{coq_example*} -Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0). +Notation "{ x : A | P }" := (sig A (fun x => P)). \end{coq_example*} In the last case though, there is a conflict with the notation for -type casts. This last notation, as shown by the command {\tt Print Grammar +type casts. The notation for type casts, as shown by the command {\tt Print Grammar constr} is at level 100. To avoid \verb=x : A= being parsed as a type cast, it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a -correct definition is +correct definition is the following. \begin{coq_example*} -Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99). +Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). \end{coq_example*} %This change has retrospectively an effect on the notation for notation @@ -182,14 +190,17 @@ Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99). %Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99). %\end{coq_example*} -See the next section for more about factorization. +More generally, it is required that notations are explicitly +factorized on the left. See the next section for more about +factorization. \subsection{Simple factorization rules} -{\Coq} extensible parsing is performed by Camlp5 which is essentially a -LL1 parser. Hence, some care has to be taken not to hide already -existing rules by new rules. Some simple left factorization work has -to be done. Here is an example. +{\Coq} extensible parsing is performed by {\camlpppp} which is +essentially a LL1 parser: it decides which notation to parse by +looking tokens from left to right. Hence, some care has to be taken +not to hide already existing rules by new rules. Some simple left +factorization work has to be done. Here is an example. \begin{coq_eval} (********** The next rule for notation _ < _ < _ produces **********) @@ -242,17 +253,19 @@ on the {\Coq} printer. For example: Check (and True True). \end{coq_example} -However, printing, especially pretty-printing, requires -more care than parsing. We may want specific indentations, -line breaks, alignment if on several lines, etc. +However, printing, especially pretty-printing, also requires some +care. We may want specific indentations, line breaks, alignment if on +several lines, etc. For pretty-printing, {\Coq} relies on {\ocaml} +formatting library, which provides indentation and automatic line +breaks depending on page width by means of {\em formatting boxes}. -The default printing of notations is very rudimentary. For printing a -notation, a {\em formatting box} is opened in such a way that if the +The default printing of notations is rudimentary. For printing a +notation, a formatting box is opened in such a way that if the notation and its arguments cannot fit on a single line, a line break is inserted before the symbols of the notation and the arguments on the next lines are aligned with the argument on the first line. -A first, simple control that a user can have on the printing of a +A first simple control that a user can have on the printing of a notation is the insertion of spaces at some places of the notation. This is performed by adding extra spaces between the symbols and parameters: each extra space (other than the single space needed @@ -277,6 +290,13 @@ Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) \end{coq_example} \end{small} +\begin{coq_example} +Check + (IF_then_else (IF_then_else True False True) + (IF_then_else True False True) + (IF_then_else True False True)). +\end{coq_example} + A {\em format} is an extension of the string denoting the notation with the possible following elements delimited by single quotes: @@ -313,22 +333,15 @@ Notations do not survive the end of sections. No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the notation. -\begin{coq_example} -Check - (IF_then_else (IF_then_else True False True) - (IF_then_else True False True) - (IF_then_else True False True)). -\end{coq_example} - \Rem Sometimes, a notation is expected only for the parser. %(e.g. because %the underlying parser of {\Coq}, namely {\camlpppp}, is LL1 and some extra %rules are needed to circumvent the absence of factorization). -To do so, the option {\em only parsing} is allowed in the list of modifiers of +To do so, the option {\tt only parsing} is allowed in the list of modifiers of \texttt{Notation}. -Conversely, the {\em only printing} can be used to declare +Conversely, the {\tt only printing} can be used to declare that a notation should only be used for printing and should not declare a parsing rule. In particular, such notations do not modify the parser. @@ -339,16 +352,16 @@ The \texttt{Infix} command is a shortening for declaring notations of infix symbols. Its syntax is \begin{quote} -\noindent\texttt{Infix "{\symbolentry}" :=} {\qualid} {\tt (} \nelist{\em modifier}{,} {\tt )}. +\noindent\texttt{Infix "{\symbolentry}" :=} {\term} {\tt (} \nelist{\em modifier}{,} {\tt )}. \end{quote} and it is equivalent to \begin{quote} -\noindent\texttt{Notation "x {\symbolentry} y" := ({\qualid} x y) (} \nelist{\em modifier}{,} {\tt )}. +\noindent\texttt{Notation "x {\symbolentry} y" := ({\term} x y) (} \nelist{\em modifier}{,} {\tt )}. \end{quote} -where {\tt x} and {\tt y} are fresh names distinct from {\qualid}. Here is an example. +where {\tt x} and {\tt y} are fresh names. Here is an example. \begin{coq_example*} Infix "/\" := and (at level 80, right associativity). @@ -380,12 +393,14 @@ reserved. Hence their precedence and associativity cannot be changed. \comindex{CoFixpoint {\ldots} where {\ldots}} \comindex{Inductive {\ldots} where {\ldots}}} -Thanks to reserved notations, the inductive, co-inductive, recursive -and corecursive definitions can benefit of customized notations. To do -this, insert a {\tt where} notation clause after the definition of the -(co)inductive type or (co)recursive term (or after the definition of -each of them in case of mutual definitions). The exact syntax is given -on Figure~\ref{notation-syntax}. Here are examples: +Thanks to reserved notations, the inductive, co-inductive, record, +recursive and corecursive definitions can benefit of customized +notations. To do this, insert a {\tt where} notation clause after the +definition of the (co)inductive type or (co)recursive term (or after +the definition of each of them in case of mutual definitions). The +exact syntax is given on Figure~\ref{notation-syntax} for inductive, +co-inductive, recursive and corecursive definitions and on +Figure~\ref{record-syntax} for records. Here are examples: \begin{coq_eval} Set Printing Depth 50. @@ -479,20 +494,28 @@ Locate "exists _ .. _ , _". \\ \\ {\modifiers} - & ::= & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \\ - & $|$ & \nelist{\ident}{,} {\tt at next level} \\ - & $|$ & {\tt at level} {\naturalnumber} \\ - & $|$ & {\tt left associativity} \\ - & $|$ & {\tt right associativity} \\ - & $|$ & {\tt no associativity} \\ + & ::= & {\tt at level} {\naturalnumber} \\ + & $|$ & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \zeroone{\binderinterp}\\ + & $|$ & \nelist{\ident}{,} {\tt at next level} \zeroone{\binderinterp}\\ + & $|$ & {\ident} {\binderinterp} \\ & $|$ & {\ident} {\tt ident} \\ - & $|$ & {\ident} {\tt binder} \\ - & $|$ & {\ident} {\tt closed binder} \\ & $|$ & {\ident} {\tt global} \\ & $|$ & {\ident} {\tt bigint} \\ + & $|$ & {\ident} \zeroone{{\tt strict}} {\tt pattern} \zeroone{{\tt at level} {\naturalnumber}}\\ + & $|$ & {\ident} {\tt binder} \\ + & $|$ & {\ident} {\tt closed binder} \\ + & $|$ & {\tt left associativity} \\ + & $|$ & {\tt right associativity} \\ + & $|$ & {\tt no associativity} \\ & $|$ & {\tt only parsing} \\ & $|$ & {\tt only printing} \\ - & $|$ & {\tt format} {\str} + & $|$ & {\tt format} {\str} \\ +\\ +\\ +{\binderinterp} + & ::= & {\tt as ident} \\ + & $|$ & {\tt as pattern} \\ + & $|$ & {\tt as strict pattern} \\ \end{tabular} \end{centerframe} \end{small} @@ -500,9 +523,93 @@ Locate "exists _ .. _ , _". \label{notation-syntax} \end{figure} -\subsection{Notations and simple binders} +\subsection{Notations and binders} + +Notations can include binders. This section lists +different ways to deal with binders. For further examples, see also +Section~\ref{RecursiveNotationsWithBinders}. + +\subsubsection{Binders bound in the notation and parsed as identifiers} -Notations can be defined for binders as in the example: +Here is the basic example of a notation using a binder: + +\begin{coq_example*} +Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) + (at level 200, x ident, A at level 200, right associativity). +\end{coq_example*} + +The binding variables in the right-hand side that occur as a parameter +of the notation (here {\tt x}) dynamically bind all the occurrences +in their respective binding scope after instantiation of the +parameters of the notation. This means that the term bound to {\tt B} can +refer to the variable name bound to {\tt x} as shown in the following +application of the notation: + +\begin{coq_example} +Check sigma z : nat, z = 0. +\end{coq_example} + +Notice the modifier {\tt x ident} in the declaration of the +notation. It tells to parse {\tt x} as a single identifier. + +\subsubsection{Binders bound in the notation and parsed as patterns} + +In the same way as patterns can be used as binders, as in {\tt fun + '(x,y) => x+y} or {\tt fun '(existT \_ x \_) => x}, notations can be +defined so that any pattern (in the sense of the entry {\pattern} of +Figure~\ref{term-syntax-aux}) can be used in place of the +binder. Here is an example: + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Notation "'subset' ' p , P " := (sig (fun p => P)) + (at level 200, p pattern, format "'subset' ' p , P"). +\end{coq_example*} + +\begin{coq_example} +Check subset '(x,y), x+y=0. +\end{coq_example} + +The modifier {\tt p pattern} in the declaration of the notation +tells to parse $p$ as a pattern. Note that a single +variable is both an identifier and a pattern, so, e.g., the following +also works: + +% Note: we rely on the notation of the standard library which does not +% print the expected output, so we hide the output. +\begin{coq_example} +Check subset 'x, x=0. +\end{coq_example} + +If one wants to prevent such a notation to be used for printing when the +pattern is reduced to a single identifier, one has to use instead +the modifier {\tt p strict pattern}. For parsing, however, a {\tt + strict pattern} will continue to include the case of a +variable. Here is an example showing the difference: + +\begin{coq_example*} +Notation "'subset_bis' ' p , P" := (sig (fun p => P)) + (at level 200, p strict pattern). +Notation "'subset_bis' p , P " := (sig (fun p => P)) + (at level 200, p ident). +\end{coq_example*} + +\begin{coq_example} +Check subset_bis 'x, x=0. +\end{coq_example} + +The default level for a {\tt pattern} is 0. One can use a different level by +using {\tt pattern at level} $n$ where the scale is the same as the one for +terms (Figure~\ref{init-notations}). + +\subsubsection{Binders bound in the notation and parsed as terms} + +Sometimes, for the sake of factorization of rules, a binder has to be +parsed as a term. This is typically the case for a notation such as +the following: \begin{coq_eval} Set Printing Depth 50. @@ -510,18 +617,53 @@ Set Printing Depth 50. (**** an incompatibility with the reserved notation ********) \end{coq_eval} \begin{coq_example*} -Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0). +Notation "{ x : A | P }" := (sig (fun x : A => P)) + (at level 0, x at level 99 as ident). +\end{coq_example*} + +This is so because the grammar also contains rules starting with +{\tt \{} and followed by a term, such as the rule for the notation + {\tt \{ A \} + \{ B \}} for the constant {\tt + sumbool}~(see Section~\ref{sumbool}). + +Then, in the rule, {\tt x ident} is replaced by {\tt x at level 99 as + ident} meaning that {\tt x} is parsed as a term at level 99 (as done +in the notation for {\tt sumbool}), but that this term has actually to +be an identifier. + +The notation {\tt \{ x | P \}} is already defined in the standard +library with the {\tt as ident} modifier. We cannot redefine it but +one can define an alternative notation, say {\tt \{ p such that P }\}, +using instead {\tt as pattern}. + +% Note, this conflicts with the default rule in the standard library, so +% we don't show the +\begin{coq_example*} +Notation "{ p 'such' 'that' P }" := (sig (fun p => P)) + (at level 0, p at level 99 as pattern). \end{coq_example*} -The binding variables in the left-hand-side that occur as a parameter -of the notation naturally bind all their occurrences appearing in -their respective scope after instantiation of the parameters of the -notation. +Then, the following works: +\begin{coq_example} +Check {(x,y) such that x+y=0}. +\end{coq_example} + +To enforce that the pattern should not be used for printing when it +is just an identifier, one could have said {\tt p at level + 99 as strict pattern}. + +Note also that in the absence of a {\tt as ident}, {\tt as strict + pattern} or {\tt as pattern} modifiers, the default is to consider +subexpressions occurring in binding position and parsed as terms to be +{\tt as ident}. + +\subsubsection{Binders not bound in the notation} +\label{NotationsWithBinders} -Contrastingly, the binding variables that are not a parameter of the -notation do not capture the variables of same name that -could appear in their scope after instantiation of the -notation. E.g., for the notation +We can also have binders in the right-hand side of a notation which +are not themselves bound in the notation. In this case, the binders +are considered up to renaming of the internal binder. E.g., for the +notation \begin{coq_example*} Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200). @@ -537,14 +679,6 @@ Set Printing Depth 50. Fail Check (exists_different p). \end{coq_example} -\Rem Binding variables must not necessarily be parsed using the -{\tt ident} entry. For factorization purposes, they can be said to be -parsed at another level (e.g. {\tt x} in \verb="{ x : A | P }"= must be -parsed at level 99 to be factorized with the notation -\verb="{ A } + { B }"= for which {\tt A} can be any term). -However, even if parsed as a term, this term must at the end be effectively -a single identifier. - \subsection{Notations with recursive patterns} \label{RecursiveNotations} @@ -565,24 +699,22 @@ notation parses any number of time (but at least one time) a sequence of expressions separated by the sequence of tokens $s$ (in the example, $s$ is just ``{\tt ;}''). -In the right-hand side, the term enclosed within {\tt ..} must be a -pattern with two holes of the form $\phi([~]_E,[~]_I)$ where the first -hole is occupied either by $x$ or by $y$ and the second hole is -occupied by an arbitrary term $t$ called the {\it terminating} -expression of the recursive notation. The subterm {\tt ..} $\phi(x,t)$ -{\tt ..} (or {\tt ..} $\phi(y,t)$ {\tt ..}) must itself occur at -second position of the same pattern where the first hole is occupied -by the other variable, $y$ or $x$. Otherwise said, the right-hand side -must contain a subterm of the form either $\phi(x,${\tt ..} -$\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..} $\phi(x,t)$ {\tt ..}$)$. -The pattern $\phi$ is the {\em iterator} of the recursive notation -and, of course, the name $x$ and $y$ can be chosen arbitrarily. - -The parsing phase produces a list of expressions which are used to -fill in order the first hole of the iterating pattern which is +The right-hand side must contain a subterm of the form either +$\phi(x,${\tt ..} $\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..} +$\phi(x,t)$ {\tt ..}$)$ where $\phi([~]_E,[~]_I)$, called the {\em + iterator} of the recursive notation is an arbitrary expression with +distinguished placeholders and +where $t$ is called the {\tt terminating expression} of the recursive +notation. In the example, we choose the name s$x$ and $y$ but in +practice they can of course be chosen arbitrarily. Note that the +placeholder $[~]_I$ has to occur only once but the $[~]_E$ can occur +several times. + +Parsing the notation produces a list of expressions which are used to +fill the first placeholder of the iterating pattern which itself is repeatedly nested as many times as the length of the list, the second -hole being the nesting point. In the innermost occurrence of the -nested iterating pattern, the second hole is finally filled with the +placeholder being the nesting point. In the innermost occurrence of the +nested iterating pattern, the second placeholder is finally filled with the terminating expression. In the example above, the iterator $\phi([~]_E,[~]_I)$ is {\tt cons @@ -609,24 +741,26 @@ notations, they can also be declared within interpretation scopes (see section \ref{scopes}). \subsection{Notations with recursive patterns involving binders} +\label{RecursiveNotationsWithBinders} Recursive notations can also be used with binders. The basic example is: \begin{coq_example*} -Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) +Notation "'exists' x .. y , p" := + (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, y binder, right associativity). \end{coq_example*} The principle is the same as in Section~\ref{RecursiveNotations} -except that in the iterator $\phi([~]_E,[~]_I)$, the first hole is a -placeholder occurring at the position of the binding variable of a {\tt +except that in the iterator $\phi([~]_E,[~]_I)$, the placeholder $[~]_E$ can +also occur in position of the binding variable of a {\tt fun} or a {\tt forall}. To specify that the part ``$x$ {\tt ..} $y$'' of the notation parses a sequence of binders, $x$ and $y$ must be marked as {\tt - binder} in the list of modifiers of the notation. Then, the list of -binders produced at the parsing phase are used to fill in the first -hole of the iterating pattern which is repeatedly nested as many times + binder} in the list of modifiers of the notation. The +binders of the parsed sequence are used to fill the occurrences of the first +placeholder of the iterating pattern which is repeatedly nested as many times as the number of binders generated. If ever the generalization operator {\tt `} (see Section~\ref{implicit-generalization}) is used in the binding list, the added binders are taken into account too. @@ -635,14 +769,14 @@ Binders parsing exist in two flavors. If $x$ and $y$ are marked as {\tt binder}, then a sequence such as {\tt a b c : T} will be accepted and interpreted as the sequence of binders {\tt (a:T) (b:T) (c:T)}. For instance, in the notation above, the syntax {\tt exists - a b : nat, a = b} is provided. + a b : nat, a = b} is valid. The variables $x$ and $y$ can also be marked as {\tt closed binder} in which case only well-bracketed binders of the form {\tt (a b c:T)} or {\tt \{a b c:T\}} etc. are accepted. With closed binders, the recursive sequence in the left-hand side can -be of the general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an +be of the more general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an arbitrary sequence of tokens. With open binders though, $s$ has to be empty. Here is an example of recursive notation with closed binders: @@ -661,6 +795,40 @@ Notation "'FUNAPP' x .. y , f" := (at level 200, x binder, y binder, right associativity). \end{coq_example*} +If an occurrence of the $[~]_E$ is not in position of a binding +variable but of a term, it is the name used in the binding which is +used. Here is an example: + +\begin{coq_example*} +Notation "'exists_non_null' x .. y , P" := + (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) + (at level 200, x binder). +\end{coq_example*} + +\subsection{Predefined entries} + +By default, sub-expressions are parsed as terms and the corresponding +grammar entry is called {\tt constr}. However, one may sometimes want +to restrict the syntax of terms in a notation. For instance, the +following notation will accept to parse only global reference in +position of {\tt x}: + +\begin{coq_example*} +Notation "'apply' f a1 .. an" := (.. (f a1) .. an) + (at level 10, f global, a1, an at level 9). +\end{coq_example*} + +In addition to {\tt global}, one can restrict the syntax of a +sub-expression by using the entry names {\tt ident} or {\tt pattern} +already seen in Section~\ref{NotationsWithBinders}, even when the +corresponding expression is not used as a binder in the right-hand +side. E.g.: + +\begin{coq_example*} +Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) + (at level 10, f ident, a1, an at level 9). +\end{coq_example*} + \subsection{Summary} \paragraph{Syntax of notations} @@ -754,7 +922,7 @@ stack by using the command {\tt Close Scope} {\scope}. \end{quote} Notice that this command does not only cancel the last {\tt Open Scope -{\scope}} but all the invocation of it. +{\scope}} but all the invocations of it. \Rem {\tt Open Scope} and {\tt Close Scope} do not survive the end of sections where they occur. When defined outside of a section, they are @@ -853,6 +1021,14 @@ Arguments scopes can be cleared with the following command: {\tt Arguments {\qualid} : clear scopes} \end{quote} +Extra argument scopes, to be used in case of coercion to Funclass +(see Chapter~\ref{Coercions-full}) or with a computed type, +can be given with + +\begin{quote} +{\tt Arguments} {\qualid} \nelist{\textunderscore {\tt \%} \scope}{} {\tt : extra scopes.} +\end{quote} + \begin{Variants} \item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} @@ -1108,7 +1284,7 @@ Check reflexive iff. \end{coq_example} An abbreviation expects no precedence nor associativity, since it -follows the usual syntax of application. Abbreviations are used as +is parsed as usual application. Abbreviations are used as much as possible by the {\Coq} printers unless the modifier \verb=(only parsing)= is given. @@ -1121,7 +1297,7 @@ abbreviation but at the time it is used. Especially, abbreviations can be bound to terms with holes (i.e. with ``\_''). The general syntax for abbreviations is \begin{quote} -\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} +\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident}{} \texttt{:=} {\term} \zeroone{{\tt (only parsing)}}~\verb=.= \end{quote} @@ -1147,13 +1323,15 @@ at the time of use of the abbreviation. %\verb=(only parsing)= is given) while syntactic definitions were not. \section{Tactic Notations +\label{Tactic-Notation} \comindex{Tactic Notation}} Tactic notations allow to customize the syntax of the tactics of the -tactic language\footnote{Tactic notations are just a simplification of -the {\tt Grammar tactic simple\_tactic} command that existed in -versions prior to version 8.0.}. Tactic notations obey the following -syntax +tactic language. +%% \footnote{Tactic notations are just a simplification of +%% the {\tt Grammar tactic simple\_tactic} command that existed in +%% versions prior to version 8.0.} +Tactic notations obey the following syntax: \medskip \noindent @@ -1196,7 +1374,9 @@ level indicates the parsing precedence of the tactic notation. This information is particularly relevant for notations of tacticals. Levels 0 to 5 are available (default is 0). To know the parsing precedences of the -existing tacticals, use the command {\tt Print Grammar tactic.} +existing tacticals, use the command +\comindex{Print Grammar tactic} + {\tt Print Grammar tactic.} Each type of tactic argument has a specific semantic regarding how it is parsed and how it is interpreted. The semantic is described in the |