diff options
| author | Clément Pit-Claudel | 2019-05-16 10:59:33 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-19 19:19:30 -0400 |
| commit | 2a4bd4861d0ebf0b5d5a63774ac964b431e94fbb (patch) | |
| tree | 8f7d4ef4117de2341fc09c856762cf12cd944873 | |
| parent | b381e8d1c601659ce1a864cc51edece23b1a7fd2 (diff) | |
[refman] Add a .. cmd:: header for Reserved Notation and Reserved Infix
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index edec13f681..cda228a7da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -327,22 +327,29 @@ symbols. Reserving notations ~~~~~~~~~~~~~~~~~~~ -A given notation may be used in different contexts. Coq expects all -uses of the notation to be defined at the same precedence and with the -same associativity. To avoid giving the precedence and associativity -every time, it is possible to declare a parsing rule in advance -without giving its interpretation. Here is an example from the initial -state of Coq. +.. cmd:: Reserved Notation @string {? (@modifiers) } -.. coqtop:: in + A given notation may be used in different contexts. Coq expects all + uses of the notation to be defined at the same precedence and with the + same associativity. To avoid giving the precedence and associativity + every time, this command declares a parsing rule (:token:`string`) in advance + without giving its interpretation. Here is an example from the initial + state of Coq. + + .. coqtop:: in + + Reserved Notation "x = y" (at level 70, no associativity). + + Reserving a notation is also useful for simultaneously defining an + inductive type or a recursive constant and a notation for it. - Reserved Notation "x = y" (at level 70, no associativity). + .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence + their precedence and associativity cannot be changed. -Reserving a notation is also useful for simultaneously defining an -inductive type or a recursive constant and a notation for it. + .. cmdv:: Reserved Infix "@symbol" {* @modifiers} -.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence - their precedence and associativity cannot be changed. + This command declares an infix parsing rule without giving its + interpretation. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |