diff options
| author | Clément Pit-Claudel | 2020-01-06 14:10:01 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-01-06 14:10:01 -0500 |
| commit | 1630da989cb0184d50d108ddb3a970f860058fb6 (patch) | |
| tree | d59ebd595b3a92d1538fad5cb4fad8c5dbf9919c | |
| parent | 95124216fba92f75e0aef97f4c0003eeb8689557 (diff) | |
| parent | 9bbbe5c49951b17d8066ece22f81f8785dbed917 (diff) | |
Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx migration.
Reviewed-by: jfehrle
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 368724f9d2..70dadedd35 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -327,11 +327,8 @@ function on type :g:`A`). The keyword :g:`fun` can be followed by several binders as given in Section :ref:`binders`. Functions over several variables are equivalent to an iteration of one-variable functions. For instance the expression -“fun :token:`ident`\ :math:`_{1}` … :token:`ident`\ :math:`_{n}` -: :token:`type` => :token:`term`” -denotes the same function as “ fun :token:`ident`\ -:math:`_{1}` : :token:`type` => … -fun :token:`ident`\ :math:`_{n}` : :token:`type` => :token:`term`”. If +:n:`fun {+ @ident__i } : @type => @term` +denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). @@ -362,15 +359,14 @@ the propositional implication and function types. Applications ------------ -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` denotes the -application of :token:`term`\ :math:`_0` to :token:`term`\ :math:`_1`. +The expression :n:`@term__fun @term` denotes the application of +:n:`@term__fun` (which is expected to have a function type) to +:token:`term`. -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ... -:token:`term`\ :math:`_n` denotes the application of the term -:token:`term`\ :math:`_0` to the arguments :token:`term`\ :math:`_1` ... then -:token:`term`\ :math:`_n`. It is equivalent to ( … ( :token:`term`\ :math:`_0` -:token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the -left. +The expression :n:`@term__fun {+ @term__i }` denotes the application +of the term :n:`@term__fun` to the arguments :n:`@term__i`. It is +equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: +associativity is to the left. The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see |