diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index f36767b207..99b9754e5e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -214,7 +214,7 @@ have to be observed for notations starting with a symbol, e.g., rules starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. -Displaying symbolic notations +Use of notations for printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The command :cmd:`Notation` has an effect both on the Coq parser and on the @@ -323,6 +323,20 @@ at the time of use of the notation. scope. Obviously, expressions printed by means of such extra printing rules will not be reparsed to the same form. + +.. note:: + + When several notations can be used to print a given term, the + notations which capture the largest subterm of the term are used + preferentially. Here is an example: + + .. coqtop:: in + + Notation "x < y" := (lt x y) (at level 70). + Notation "x < y < z" := (lt x y /\ lt y z) (at level 70, y at next level). + + Check (0 < 1 /\ 1 < 2). + The Infix command ~~~~~~~~~~~~~~~~~~ |