diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 346 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 30 |
4 files changed, 190 insertions, 214 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index c8c3e37efb..381f8bb661 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1025,21 +1025,21 @@ Template polymorphism Inductive types can be made polymorphic over their arguments in :math:`\Type`. -.. opt:: Auto Template Polymorphism +.. flag:: Auto Template Polymorphism - This option, enabled by default, makes every inductive type declared - at level :math:`Type` (without annotations or hiding it behind a - definition) template polymorphic. + This option, enabled by default, makes every inductive type declared + at level :math:`Type` (without annotations or hiding it behind a + definition) template polymorphic. - This can be prevented using the ``notemplate`` attribute. + This can be prevented using the ``notemplate`` attribute. - An inductive type can be forced to be template polymorphic using the - ``template`` attribute. + An inductive type can be forced to be template polymorphic using the + ``template`` attribute. - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``template`` attribute. + Template polymorphism and universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the later is + enabled it will prevail over automatic template polymorphism and + cause an error when using the ``template`` attribute. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. @@ -1120,7 +1120,7 @@ and otherwise in the Type hierarchy. Note that the side-condition about allowed elimination sorts in the rule **Ind-Family** is just to avoid to recompute the allowed elimination -sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). As +sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As an example, let us consider the following definition: .. example:: @@ -1244,7 +1244,7 @@ primitive recursion over the structure. But this operator is rather tedious to implement and use. We choose in this version of |Coq| to factorize the operator for primitive recursion into two more primitive operations as was first suggested by Th. -Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The +Coquand in :cite:`Coq92`. One is the definition by pattern matching. The second one is a definition by guarded fixpoints. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 320448d46e..85474a3e98 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -618,7 +618,7 @@ Finally, it gives the definition of the usual orderings ``le``, Properties of these relations are not initially known, but may be required by the user from modules ``Le`` and ``Lt``. Finally, -``Peano`` gives some lemmas allowing pattern-matching, and a double +``Peano`` gives some lemmas allowing pattern matching, and a double induction principle. .. index:: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 27ed176a9b..636144e0c8 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -100,19 +100,25 @@ to be all present if the missing ones can be inferred or prompted for Rat_bottom_cond := O_S 1; Rat_irred_cond := one_two_irred |}. -This syntax can be disabled globally for printing by +The following settings let you control the display format for types: -.. cmd:: Unset Printing Records +.. flag:: Printing Records -For a given type, one can override this using either + If set, use the record syntax (shown above) as the default display format. -.. cmd:: Add Printing Record @ident +You can override the display format for specified types by adding entries to these tables: -to get record syntax or +.. table:: Printing Record @qualid + :name: Printing Record -.. cmd:: Add Printing Constructor @ident + Specifies a set of qualids which are displayed as records. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. -to get constructor syntax. +.. table:: Printing Constructor @qualid + :name: Printing Constructor + + Specifies a set of qualids which are displayed as constructors. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. This syntax can also be used for pattern matching. @@ -145,7 +151,7 @@ available: It can be activated for printing with -.. opt:: Printing Projections +.. flag:: Printing Projections .. example:: @@ -221,35 +227,35 @@ the errors of inductive definitions, as described in Section Primitive Projections ~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Primitive Projections +.. flag:: Primitive Projections -Turns on the use of primitive -projections when defining subsequent records (even through the ``Inductive`` -and ``CoInductive`` commands). Primitive projections -extended the Calculus of Inductive Constructions with a new binary -term constructor `r.(p)` representing a primitive projection `p` applied -to a record object `r` (i.e., primitive projections are always applied). -Even if the record type has parameters, these do not appear at -applications of the projection, considerably reducing the sizes of -terms when manipulating parameterized records and type checking time. -On the user level, primitive projections can be used as a replacement -for the usual defined ones, although there are a few notable differences. + Turns on the use of primitive + projections when defining subsequent records (even through the ``Inductive`` + and ``CoInductive`` commands). Primitive projections + extended the Calculus of Inductive Constructions with a new binary + term constructor `r.(p)` representing a primitive projection `p` applied + to a record object `r` (i.e., primitive projections are always applied). + Even if the record type has parameters, these do not appear at + applications of the projection, considerably reducing the sizes of + terms when manipulating parameterized records and type checking time. + On the user level, primitive projections can be used as a replacement + for the usual defined ones, although there are a few notable differences. -.. opt:: Printing Primitive Projection Parameters +.. flag:: Printing Primitive Projection Parameters -This compatibility option reconstructs internally omitted parameters at -printing time (even though they are absent in the actual AST manipulated -by the kernel). + This compatibility option reconstructs internally omitted parameters at + printing time (even though they are absent in the actual AST manipulated + by the kernel). -.. opt:: Printing Primitive Projection Compatibility +.. flag:: Printing Primitive Projection Compatibility -This compatibility option (on by default) governs the -printing of pattern-matching over primitive records. + This compatibility option (on by default) governs the + printing of pattern matching over primitive records. Primitive Record Types ++++++++++++++++++++++ -When the :opt:`Primitive Projections` option is on, definitions of +When the :flag:`Primitive Projections` option is on, definitions of record types change meaning. When a type is declared with primitive projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). To eliminate the (co-)inductive type, one must use its defined primitive projections. @@ -259,9 +265,9 @@ To eliminate the (co-)inductive type, one must use its defined primitive project For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the -``Printing Primitive Projection Parameters`` flag. Further compatibility +:flag:`Printing Primitive Projection Parameters` flag. Further compatibility printing can be deactivated thanks to the ``Printing Primitive Projection -Compatibility`` option which governs the printing of pattern-matching +Compatibility`` option which governs the printing of pattern matching over primitive records. There are currently two ways to introduce primitive records types: @@ -291,7 +297,7 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the ``Printing Primitive Projection Compatibility`` +user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` to display unfolded primitive projections as matches and distinguish them from folded ones. @@ -304,7 +310,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the ``Printing Primitive Projection Parameters`` option +projection if the :flag`Printing Primitive Projection Parameters` option is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -318,17 +324,17 @@ Variants and extensions of :g:`match` .. _mult-match: -Multiple and nested pattern-matching +Multiple and nested pattern matching ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The basic version of :g:`match` allows pattern-matching on simple +The basic version of :g:`match` allows pattern matching on simple patterns. As an extension, multiple nested patterns or disjunction of patterns are allowed, as in ML-like languages. The extension just acts as a macro that is expanded during parsing into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed -under its expanded form (see :opt:`Printing Matching`). +under its expanded form (see :flag:`Printing Matching`). .. seealso:: :ref:`extendedpatternmatching`. @@ -337,7 +343,7 @@ under its expanded form (see :opt:`Printing Matching`). Pattern-matching on boolean values: the if expression ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For inductive types with exactly two constructors and for pattern-matching +For inductive types with exactly two constructors and for pattern matching expressions that do not depend on the arguments of the constructors, it is possible to use a ``if … then … else`` notation. For instance, the definition @@ -476,123 +482,93 @@ of :g:`match` expressions. Printing nested patterns +++++++++++++++++++++++++ -.. opt:: Printing Matching +.. flag:: Printing Matching -The Calculus of Inductive Constructions knows pattern-matching only -over simple patterns. It is however convenient to re-factorize nested -pattern-matching into a single pattern-matching over a nested -pattern. + The Calculus of Inductive Constructions knows pattern matching only + over simple patterns. It is however convenient to re-factorize nested + pattern matching into a single pattern matching over a nested + pattern. -When this option is on (default), |Coq|’s printer tries to do such -limited re-factorization. -Turning it off tells |Coq| to print only simple pattern-matching problems -in the same way as the |Coq| kernel handles them. + When this option is on (default), |Coq|’s printer tries to do such + limited re-factorization. + Turning it off tells |Coq| to print only simple pattern matching problems + in the same way as the |Coq| kernel handles them. Factorization of clauses with same right-hand side ++++++++++++++++++++++++++++++++++++++++++++++++++ -.. opt:: Printing Factorizable Match Patterns +.. flag:: Printing Factorizable Match Patterns -When several patterns share the same right-hand side, it is additionally -possible to share the clauses using disjunctive patterns. Assuming that the -printing matching mode is on, this option (on by default) tells |Coq|'s -printer to try to do this kind of factorization. + When several patterns share the same right-hand side, it is additionally + possible to share the clauses using disjunctive patterns. Assuming that the + printing matching mode is on, this option (on by default) tells |Coq|'s + printer to try to do this kind of factorization. Use of a default clause +++++++++++++++++++++++ -.. opt:: Printing Allow Default Clause +.. flag:: Printing Allow Match Default Clause -When several patterns share the same right-hand side which do not depend on the -arguments of the patterns, yet an extra factorization is possible: the -disjunction of patterns can be replaced with a `_` default clause. Assuming that -the printing matching mode and the factorization mode are on, this option (on by -default) tells |Coq|'s printer to use a default clause when relevant. + When several patterns share the same right-hand side which do not depend on the + arguments of the patterns, yet an extra factorization is possible: the + disjunction of patterns can be replaced with a `_` default clause. Assuming that + the printing matching mode and the factorization mode are on, this option (on by + default) tells |Coq|'s printer to use a default clause when relevant. Printing of wildcard patterns ++++++++++++++++++++++++++++++ -.. opt:: Printing Wildcard +.. flag:: Printing Wildcard -Some variables in a pattern may not occur in the right-hand side of -the pattern-matching clause. When this option is on (default), the -variables having no occurrences in the right-hand side of the -pattern-matching clause are just printed using the wildcard symbol -“_”. + Some variables in a pattern may not occur in the right-hand side of + the pattern matching clause. When this option is on (default), the + variables having no occurrences in the right-hand side of the + pattern matching clause are just printed using the wildcard symbol + “_”. Printing of the elimination predicate +++++++++++++++++++++++++++++++++++++ -.. opt:: Printing Synth +.. flag:: Printing Synth -In most of the cases, the type of the result of a matched term is -mechanically synthesizable. Especially, if the result type does not -depend of the matched term. When this option is on (default), -the result type is not printed when |Coq| knows that it can re- -synthesize it. + In most of the cases, the type of the result of a matched term is + mechanically synthesizable. Especially, if the result type does not + depend of the matched term. When this option is on (default), + the result type is not printed when |Coq| knows that it can re- + synthesize it. Printing matching on irrefutable patterns ++++++++++++++++++++++++++++++++++++++++++ -If an inductive type has just one constructor, pattern-matching can be +If an inductive type has just one constructor, pattern matching can be written using the first destructuring let syntax. -.. cmd:: Add Printing Let @ident - - This adds `ident` to the list of inductive types for which pattern-matching - is written using a let expression. - -.. cmd:: Remove Printing Let @ident - - This removes ident from this list. Note that removing an inductive - type from this list has an impact only for pattern-matching written - using :g:`match`. Pattern-matching explicitly written using a destructuring - :g:`let` are not impacted. - -.. cmd:: Test Printing Let for @ident - - This tells if `ident` belongs to the list. - -.. cmd:: Print Table Printing Let - - This prints the list of inductive types for which pattern-matching is - written using a let expression. +.. table:: Printing Let @qualid + :name: Printing Let - The list of inductive types for which pattern-matching is written - using a :g:`let` expression is managed synchronously. This means that it is - sensitive to the command ``Reset``. + Specifies a set of qualids for which pattern matching is displayed using a let expression. + Note that this only applies to pattern matching instances entered with :g:`match`. + It doesn't affect pattern matching explicitly entered with a destructuring + :g:`let`. + Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set. Printing matching on booleans +++++++++++++++++++++++++++++ -If an inductive type is isomorphic to the boolean type, pattern-matching -can be written using ``if`` … ``then`` … ``else`` …: +If an inductive type is isomorphic to the boolean type, pattern matching +can be written using ``if`` … ``then`` … ``else`` …. This table controls +which types are written this way: -.. cmd:: Add Printing If @ident +.. table:: Printing If @qualid + :name: Printing If - This adds ident to the list of inductive types for which pattern-matching is - written using an if expression. - -.. cmd:: Remove Printing If @ident - - This removes ident from this list. - -.. cmd:: Test Printing If for @ident - - This tells if ident belongs to the list. - -.. cmd:: Print Table Printing If - - This prints the list of inductive types for which pattern-matching is - written using an if expression. - -The list of inductive types for which pattern-matching is written -using an ``if`` expression is managed synchronously. This means that it is -sensitive to the command ``Reset``. + Specifies a set of qualids for which pattern matching is displayed using + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` + commands to update this set. This example emphasizes what the printing options offer. @@ -674,7 +650,7 @@ than like this: *Limitations* -|term_0| must be built as a *pure pattern-matching tree* (:g:`match … with`) +|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being @@ -702,7 +678,7 @@ terminating functions. - the definition uses pattern matching on dependent types, which ``Function`` cannot deal with yet. - - the definition is not a *pattern-matching tree* as explained above. + - the definition is not a *pattern matching tree* as explained above. .. warn:: Cannot define principle(s) for @ident. @@ -1240,7 +1216,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. Prints the module type corresponding to :n:`@ident`. -.. opt:: Short Module Printing +.. flag:: Short Module Printing This option (off by default) disables the printing of the types of fields, leaving only their names, for the commands :cmd:`Print Module` and @@ -1515,7 +1491,7 @@ says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option. +:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` option. .. seealso:: :ref:`displaying-implicit-args`. @@ -1747,65 +1723,65 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Implicit Arguments +.. flag:: Implicit Arguments -This option (off by default) allows to systematically declare implicit -the arguments detectable as such. Auto-detection of implicit arguments is -governed by options controlling whether strict and contextual implicit -arguments have to be considered or not. + This option (off by default) allows to systematically declare implicit + the arguments detectable as such. Auto-detection of implicit arguments is + governed by options controlling whether strict and contextual implicit + arguments have to be considered or not. .. _controlling-strict-implicit-args: Controlling strict implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Strict Implicit +.. flag:: Strict Implicit -When the mode for automatic declaration of implicit arguments is on, -the default is to automatically set implicit only the strict implicit -arguments plus, for historical reasons, a small subset of the non-strict -implicit arguments. To relax this constraint and to set -implicit all non strict implicit arguments by default, you can turn this -option off. + When the mode for automatic declaration of implicit arguments is on, + the default is to automatically set implicit only the strict implicit + arguments plus, for historical reasons, a small subset of the non-strict + implicit arguments. To relax this constraint and to set + implicit all non strict implicit arguments by default, you can turn this + option off. -.. opt:: Strongly Strict Implicit +.. flag:: Strongly Strict Implicit -Use this option (off by default) to capture exactly the strict implicit -arguments and no more than the strict implicit arguments. + Use this option (off by default) to capture exactly the strict implicit + arguments and no more than the strict implicit arguments. .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Contextual Implicit +.. flag:: Contextual Implicit -By default, |Coq| does not automatically set implicit the contextual -implicit arguments. You can turn this option on to tell |Coq| to also -infer contextual implicit argument. + By default, |Coq| does not automatically set implicit the contextual + implicit arguments. You can turn this option on to tell |Coq| to also + infer contextual implicit argument. .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Reversible Pattern Implicit +.. flag:: Reversible Pattern Implicit -By default, |Coq| does not automatically set implicit the reversible-pattern -implicit arguments. You can turn this option on to tell |Coq| to also infer -reversible-pattern implicit argument. + By default, |Coq| does not automatically set implicit the reversible-pattern + implicit arguments. You can turn this option on to tell |Coq| to also infer + reversible-pattern implicit argument. .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Maximal Implicit Insertion +.. flag:: Maximal Implicit Insertion -Assuming the implicit argument mode is on, this option (off by default) -declares implicit arguments to be automatically inserted when a -function is partially applied and the next argument of the function is -an implicit one. + Assuming the implicit argument mode is on, this option (off by default) + declares implicit arguments to be automatically inserted when a + function is partially applied and the next argument of the function is + an implicit one. .. _explicit-applications: @@ -1877,20 +1853,20 @@ if each of them is to be used maximally or not, use the command Explicit displaying of implicit arguments for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Implicit +.. flag:: Printing Implicit -By default, the basic pretty-printing rules hide the inferable implicit -arguments of an application. Turn this option on to force printing all -implicit arguments. + By default, the basic pretty-printing rules hide the inferable implicit + arguments of an application. Turn this option on to force printing all + implicit arguments. -.. opt:: Printing Implicit Defensive +.. flag:: Printing Implicit Defensive -By default, the basic pretty-printing rules display the implicit -arguments that are not detected as strict implicit arguments. This -“defensive” mode can quickly make the display cumbersome so this can -be deactivated by turning this option off. + By default, the basic pretty-printing rules display the implicit + arguments that are not detected as strict implicit arguments. This + “defensive” mode can quickly make the display cumbersome so this can + be deactivated by turning this option off. -.. seealso:: :opt:`Printing All`. +.. seealso:: :flag:`Printing All`. Interaction with subtyping ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1915,14 +1891,14 @@ but succeeds in Deactivation of implicit arguments for parsing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Parsing Explicit +.. flag:: Parsing Explicit -Turning this option on (it is off by default) deactivates the use of implicit arguments. + Turning this option on (it is off by default) deactivates the use of implicit arguments. -In this case, all arguments of constants, inductive types, -constructors, etc, including the arguments declared as implicit, have -to be given as if no arguments were implicit. By symmetry, this also -affects printing. + In this case, all arguments of constants, inductive types, + constructors, etc, including the arguments declared as implicit, have + to be given as if no arguments were implicit. By symmetry, this also + affects printing. Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -2134,32 +2110,32 @@ to coercions are provided in :ref:`implicitcoercions`. Printing constructions in full ------------------------------ -.. opt:: Printing All +.. flag:: Printing All -Coercions, implicit arguments, the type of pattern-matching, but also -notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some -tactics (typically the tactics applying to occurrences of subterms are -sensitive to the implicit arguments). Turning this option on -deactivates all high-level printing features such as coercions, -implicit arguments, returned type of pattern-matching, notations and -various syntactic sugar for pattern-matching or record projections. -Otherwise said, :opt:`Printing All` includes the effects of the options -:opt:`Printing Implicit`, :opt:`Printing Coercions`, :opt:`Printing Synth`, -:opt:`Printing Projections`, and :opt:`Printing Notations`. To reactivate -the high-level printing features, use the command ``Unset Printing All``. + Coercions, implicit arguments, the type of pattern matching, but also + notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some + tactics (typically the tactics applying to occurrences of subterms are + sensitive to the implicit arguments). Turning this option on + deactivates all high-level printing features such as coercions, + implicit arguments, returned type of pattern matching, notations and + various syntactic sugar for pattern matching or record projections. + Otherwise said, :flag:`Printing All` includes the effects of the options + :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`, + :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate + the high-level printing features, use the command ``Unset Printing All``. .. _printing-universes: Printing universes ------------------ -.. opt:: Printing Universes +.. flag:: Printing Universes -Turn this option on to activate the display of the actual level of each -occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in -combination with :opt:`Printing All` can help to diagnose failures to unify -terms apparently identical but internally different in the Calculus of Inductive -Constructions. + Turn this option on to activate the display of the actual level of each + occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in + combination with :flag:`Printing All` can help to diagnose failures to unify + terms apparently identical but internally different in the Calculus of Inductive + Constructions. The constraints on the internal level of the occurrences of Type (see :ref:`Sorts`) can be printed using the command @@ -2221,7 +2197,7 @@ form is appending to its name, indicating how the variables of its defining context are instantiated. The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the flag ``Printing Existential Instances`` +instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` is on (see Section :ref:`explicit-display-existentials`), and this is why an existential variable used in the same context as its context of definition is written with no instance. @@ -2243,11 +2219,11 @@ with a named-goal selector, see :ref:`goal-selectors`). Explicit displaying of existential instances for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Existential Instances +.. flag:: Printing Existential Instances -This option (off by default) activates the full display of how the -context of an existential variable is instantiated at each of the -occurrences of the existential variable. + This option (off by default) activates the full display of how the + context of an existential variable is instantiated at each of the + occurrences of the existential variable. .. _tactics-in-terms: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ad7b5c82fd..daf34500bf 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -374,13 +374,13 @@ Definition by case analysis --------------------------- Objects of inductive types can be destructurated by a case-analysis -construction called *pattern-matching* expression. A pattern-matching +construction called *pattern matching* expression. A pattern matching expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly. -This paragraph describes the basic form of pattern-matching. See +This paragraph describes the basic form of pattern matching. See Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description -of the general form. The basic form of pattern-matching is characterized +of the general form. The basic form of pattern matching is characterized by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form :n:`@qualid {* @ident}`. @@ -388,9 +388,9 @@ single :token:`pattern` and :token:`pattern` restricted to the form The expression match ":token:`term`:math:`_0` :token:`return_type` with :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|` :token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a -*pattern-matching* over the term :token:`term`:math:`_0` (expected to be +*pattern matching* over the term :token:`term`:math:`_0` (expected to be of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\ -:token:`term`:math:`_n` are the *branches* of the pattern-matching +:token:`term`:math:`_n` are the *branches* of the pattern matching expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid` :token:`ident` where :token:`qualid` must denote a constructor. There should be exactly one branch for every constructor of :math:`I`. @@ -403,7 +403,7 @@ inferred from the type of the branches [2]_. In the *dependent* case, there are three subcases. In the first subcase, the type in each branch may depend on the exact value being matched in -the branch. In this case, the whole pattern-matching itself depends on +the branch. In this case, the whole pattern matching itself depends on the term being matched. This dependency of the term being matched in the return type is expressed with an “as :token:`ident`” clause where :token:`ident` is dependent in the return type. For instance, in the following example: @@ -424,7 +424,7 @@ is dependent in the return type. For instance, in the following example: the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" and ":g:`or (eq bool false true) (eq bool false false)`" while the whole -pattern-matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", +pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", the identifier :g:`b` being used to represent the dependency. .. note:: @@ -447,7 +447,7 @@ as the equality predicate (see Section :ref:`coq-equality`), the order predicate on natural numbers or the type of lists of a given length (see Section :ref:`matching-dependent`). In this configuration, the type of each branch can depend on the type dependencies specific to the -branch and the whole pattern-matching expression has a type determined +branch and the whole pattern matching expression has a type determined by the specific dependencies in the type of the term being matched. This dependency of the return type in the annotations of the inductive type is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` … @@ -476,13 +476,13 @@ For instance, in the following example: the type of the branch is :g:`eq A x x` because the third argument of :g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the -type of the whole pattern-matching expression has type :g:`eq A y x` because the +type of the whole pattern matching expression has type :g:`eq A y x` because the third argument of eq is y in the type of H. This dependency of the case analysis in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the return type. Finally, the third subcase is a combination of the first and second -subcase. In particular, it only applies to pattern-matching on terms in +subcase. In particular, it only applies to pattern matching on terms in a type with annotations. For this third subcase, both the clauses ``as`` and ``in`` are available. @@ -943,7 +943,7 @@ Parametrized inductive types sort for the inductive definition and will produce a less convenient rule for case elimination. -.. opt:: Uniform Inductive Parameters +.. flag:: Uniform Inductive Parameters When this option is set (it is off by default), inductive definitions are abstracted over their parameters @@ -980,7 +980,7 @@ Variants The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except that it disallows recursive definition of types (for instance, lists cannot be defined using :cmd:`Variant`). No induction scheme is generated for - this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on. + this variant, unless option :flag:`Nonrecursive Elimination Schemes` is on. .. exn:: The @num th argument of @ident must be @ident in @type. :undocumented: @@ -1126,7 +1126,7 @@ constructions. .. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term - This command allows defining functions by pattern-matching over inductive + This command allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define :token:`ident` a recursive function with arguments specified by the :token:`binders` such that :token:`ident` applied to arguments @@ -1329,7 +1329,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: You are asserting a new statement while already being in proof editing mode. This feature, called nested proofs, is disabled by default. - To activate it, turn option :opt:`Nested Proofs Allowed` on. + To activate it, turn option :flag:`Nested Proofs Allowed` on. .. cmdv:: Lemma @ident {? @binders } : @type Remark @ident {? @binders } : @type @@ -1403,7 +1403,7 @@ using the keyword :cmd:`Qed`. .. note:: #. Several statements can be simultaneously asserted provided option - :opt:`Nested Proofs Allowed` was turned on. + :flag:`Nested Proofs Allowed` was turned on. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the |