diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 7c628e534b..8bfcab0f4e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -417,6 +417,27 @@ identifiers or tokens starting with a single quote are dropped. Locate "exists". Locate "exists _ .. _ , _". +Inheritance of the properties of arguments of constants bound to a notation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +If the right-hand side of a notation is a partially applied constant, +the notation inherits the implicit arguments (see +:ref:`ImplicitArguments`) and interpretation scopes (see +:ref:`Scopes`) of the constant. For instance: + +.. coqtop:: in reset + + Record R := {dom : Type; op : forall {A}, A -> dom}. + Notation "# x" := (@op x) (at level 8). + +.. coqtop:: all + + Check fun x:R => # x 3. + +As an exception, if the right-hand side is just of the form +:n:`@@qualid`, this conventionally stops the inheritance of implicit +arguments (but not of interpretation scopes). + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -1415,6 +1436,12 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + Like for notations, if the right-hand side of an abbreviation is a + partially applied constant, the abbreviation inherits the implicit + arguments and interpretation scopes of the constant. As an + exception, if the right-hand side is just of the form :n:`@@qualid`, + this conventionally stops the inheritance of implicit arguments. + .. _numeral-notations: Numeral notations |