diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-23 19:08:15 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:08 +0100 |
commit | 79a03d8a491cb153c182c48e2c8a388d682bfcf4 (patch) | |
tree | 1ecab02f434a9ead250e0abdbf1d1a38cd89c1ea /doc | |
parent | c1359f0ec2a77210ec80ad44753817418f102270 (diff) |
Documenting use of primitive entry names for restricting syntax in notations.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-syn.tex | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index da6028126..a4ed2134e 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -658,6 +658,7 @@ subexpressions occurring in binding position and parsed as terms to be {\tt as ident}. \subsubsection{Binders not bound in the notation} +\label{NotationsWithBinders} 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 @@ -804,6 +805,30 @@ Notation "'exists_non_null' x .. y , 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} |