diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-09 13:50:22 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-09 15:40:20 +0100 |
commit | b7415c84269b1553470216b06871def933e2f3bd (patch) | |
tree | 15c640670945dde7a431e622004e3a1fb1bdc0ee /doc | |
parent | 76fc1698fbb6b523c5c0d15f0b15a2d035649496 (diff) |
Clarifying doc about interpretation of scopes in notations (#5386).
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-syn.tex | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 21c39de96..b7d36ecaa 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -59,6 +59,12 @@ and pretty-printer of {\Coq} already know how to deal with the 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 +Section~\ref{Implicit Arguments}), coercions (see +Section~\ref{Coercions}), etc. are resolved at the time of the +declaration of the notation. + \subsection[Precedences and associativity]{Precedences and associativity\index{Precedences} \index{Associativity}} @@ -908,6 +914,28 @@ interpretation. See the next section. \SeeAlso The command to show the scopes bound to the arguments of a function is described in Section~\ref{About}. +\Rem In notations, the subterms matching the identifiers of the +notations are interpreted in the scope in which the identifiers +occurred at the time of the declaration of the notation. Here is an +example: + +\begin{coq_example} +Parameter g : bool -> bool. +Notation "@@" := true (only parsing) : bool_scope. +Notation "@@" := false (only parsing): mybool_scope. + +(* Defining a notation while the argument of g is bound to bool_scope *) +Bind Scope bool_scope with bool. +Notation "# x #" := (g x) (at level 40). +Check # @@ #. +(* Rebinding the argument of g to mybool_scope has no effect on the notation *) +Arguments g _%mybool_scope. +Check # @@ #. +(* But we can force the scope *) +Delimit Scope mybool_scope with mybool. +Check # @@%mybool #. +\end{coq_example} + \subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope@\texttt{type\_scope}}} The scope {\tt type\_scope} has a special status. It is a primitive |