diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/language/core/coinductive.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/language/core/index.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/core/primitive.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sections.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/index.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 39 |
17 files changed, 129 insertions, 66 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 41e1c30f0d..a38282d41a 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -117,7 +117,7 @@ Assumptions Assumptions extend the environment with axioms, parameters, hypotheses or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted -by Coq if and only if this :n:`@type` is a correct type in the environment +by |Coq| if and only if this :n:`@type` is a correct type in the environment preexisting the declaration and if :n:`@ident` was not previously defined in the same module. This :n:`@type` is considered to be the type (or specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` @@ -141,8 +141,8 @@ has type :n:`@type`. of_type ::= {| : | :> } @type These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in - the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence - of an object of this type) is accepted as a postulate. + the global context. The fact asserted by :n:`@type` (or, equivalently, the existence + of an object of this type) is accepted as a postulate. They accept the :attr:`program` attribute. :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms are equivalent. They can take the :attr:`local` :term:`attribute`, @@ -155,6 +155,10 @@ has type :n:`@type`. is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly parameterized (i.e., the variables are *discharged*). See Section :ref:`section-mechanism`. + :n:`:>` + If specified, :token:`ident_decl` is automatically + declared as a coercion to the class of its type. See :ref:`coercions`. + The :n:`Inline` clause is only relevant inside functors. See :cmd:`Module`. .. example:: Simple assumptions diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 45bdc019ac..29a2b40162 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -134,7 +134,7 @@ Numbers hexdigit ::= {| 0 .. 9 | a .. f | A .. F } :n:`@integer` and :n:`@natural` are limited to the range that fits - into an OCaml integer (63-bit integers on most architectures). + into an |OCaml| integer (63-bit integers on most architectures). :n:`@bigint` and :n:`@bignat` have no range limitation. The :ref:`standard library <thecoqlibrary>` provides some @@ -152,8 +152,8 @@ Strings :token:`string`. Keywords - The following character sequences are keywords defined in the main Coq grammar - that cannot be used as identifiers (even when starting Coq with the `-noinit` + The following character sequences are keywords defined in the main |Coq| grammar + that cannot be used as identifiers (even when starting |Coq| with the `-noinit` command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop @@ -168,11 +168,11 @@ Keywords keywords. Other tokens - The following character sequences are tokens defined in the main Coq grammar - (even when starting Coq with the `-noinit` command-line flag):: + The following character sequences are tokens defined in the main |Coq| grammar + (even when starting |Coq| with the `-noinit` command-line flag):: ! #[ % & ' ( () ) * + , - -> - . .( .. ... / : ::= := :> :>> ; < <+ <- <: + . .( .. ... / : ::= := :> ; < <+ <- <: <<: <= = => > >-> >= ? @ @{ [ ] _ `( `{ { {| | } @@ -325,10 +325,10 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types boldface label "Command:". Commands are listed in the :ref:`command_index`. Example: - .. cmd:: Comments {* @string } + .. cmd:: Comments {* {| @one_term | @string | @natural } } - This command prints "Comments ok" and does not change anything - to the state of the document. + Prints "Comments ok" and does not change + the state of the document. tactic diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index c034b7f302..2e5dff42ac 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -28,8 +28,8 @@ More information on co-inductive definitions can be found in This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, :attr:`universes(template)`, :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(noncumulative)`, :attr:`private(matching)` + and :attr:`using` attributes. .. example:: @@ -76,7 +76,7 @@ propositional η-equality, which itself would require full η-conversion for subject reduction to hold, but full η-conversion is not acceptable as it would make type checking undecidable. -Since the introduction of primitive records in Coq 8.5, an alternative +Since the introduction of primitive records in |Coq| 8.5, an alternative presentation is available, called *negative co-inductive types*. This consists in defining a co-inductive type as a primitive record type through its projections. Such a technique is akin to the *co-pattern* style that can be @@ -115,7 +115,7 @@ equality: Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. -As of Coq 8.9, it is now advised to use negative co-inductive types rather than +As of |Coq| 8.9, it is now advised to use negative co-inductive types rather than their positive counterparts. .. seealso:: @@ -195,7 +195,7 @@ Top-level definitions of co-recursive functions As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously defining several mutual cofixpoints. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 42203d9d65..1681eee6e7 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -87,10 +87,10 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` and - :attr:`canonical` attributes. + :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`canonical` and :attr:`using` attributes. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -135,11 +135,13 @@ Chapter :ref:`Tactics`. The basic assertion command is: | Proposition | Property - After the statement is asserted, Coq needs a proof. Once a proof of + After the statement is asserted, |Coq| needs a proof. Once a proof of :n:`@type` under the assumptions represented by :n:`@binder`\s is given and validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and the theorem is bound to the name :n:`@ident` in the environment. + These commands accept the :attr:`program` attribute. See :ref:`program_lemma`. + Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction over a mutually inductive assumption, or that assert mutually dependent statements in some mutual co-inductive type. It is equivalent to @@ -157,6 +159,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. + This command accepts the :attr:`using` attribute. + .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: @@ -172,7 +176,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: This feature, called nested proofs, is disabled by default. To activate it, turn the :flag:`Nested Proofs Allowed` flag on. -Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +Proofs start with the keyword :cmd:`Proof`. Then |Coq| enters the proof editing mode until the proof is completed. In proof editing mode, the user primarily enters tactics, which are described in chapter :ref:`Tactics`. The user may also enter commands to manage the proof editing mode. They are described in Chapter diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst index de780db267..c7b1df28db 100644 --- a/doc/sphinx/language/core/index.rst +++ b/doc/sphinx/language/core/index.rst @@ -4,7 +4,7 @@ Core language ============= -At the heart of the Coq proof assistant is the Coq kernel. While +At the heart of the |Coq| proof assistant is the |Coq| kernel. While users have access to a language with many convenient features such as :ref:`notations <syntax-extensions-and-notation-scopes>`, :ref:`implicit arguments <ImplicitArguments>`, etc. (presented in the diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 39b154de8d..1642482bb1 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -17,7 +17,7 @@ Inductive types constructor ::= @ident {* @binder } {? @of_type } This command defines one or more - inductive types and its constructors. Coq generates destructors + inductive types and its constructors. |Coq| generates destructors depending on the universe that the inductive type belongs to. The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``, @@ -342,9 +342,9 @@ Recursive functions: fix .. insertprodn term_fix fixannot .. prodn:: - term_fix ::= let fix @fix_body in @term - | fix @fix_body {? {+ with @fix_body } for @ident } - fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term + term_fix ::= let fix @fix_decl in @term + | fix @fix_decl {? {+ with @fix_decl } for @ident } + fix_decl ::= @ident {* @binder } {? @fixannot } {? : @type } := @term fixannot ::= %{ struct @ident %} | %{ wf @one_term @ident %} | %{ measure @one_term {? @ident } {? @one_term } %} @@ -361,7 +361,11 @@ syntax: :n:`let fix @ident {* @binder } := @term in` stands for Some options of :n:`@fixannot` are only supported in specific constructs. :n:`fix` and :n:`let fix` only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in -commands such as :cmd:`Function` and :cmd:`Program Fixpoint`. +commands such as :cmd:`Fixpoint` (with the :attr:`program` attribute) and :cmd:`Function`. + +.. todo explanation of struct: see text above at the Fixpoint command, also + see https://github.com/coq/coq/pull/12936#discussion_r510716268 and above. + Consider whether to move the grammar for fixannot elsewhere .. _Fixpoint: @@ -379,7 +383,7 @@ constructions. .. prodn:: fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } - This command allows defining functions by pattern matching over inductive + Allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define :n:`@ident` as a recursive function with arguments specified by the :n:`@binder`\s such that :n:`@ident` applied to arguments @@ -388,6 +392,8 @@ constructions. consequently :n:`forall {* @binder }, @type` and its value is equivalent to :n:`fun {* @binder } => @term`. + This command accepts the :attr:`program` attribute. + To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They are needed to ensure that the :cmd:`Fixpoint` definition always terminates. @@ -399,17 +405,19 @@ constructions. that satisfies the decreasing condition. :cmd:`Fixpoint` without the :attr:`program` attribute does not support the - :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. + :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`. The :n:`with` clause allows simultaneously defining several mutual fixpoints. It is especially useful when defining functions over mutually defined inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + This command accepts the :attr:`using` attribute. + .. note:: + Some fixpoints may have several arguments that fit as decreasing diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 866104d5d1..1309a47ff4 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -1001,12 +1001,12 @@ of the ``Require`` command can be used to bypass the implicit shortening by providing an absolute root to the required file (see :ref:`compiled-files`). There also exists another independent loadpath mechanism attached to -OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object -files as described above. The OCaml loadpath is managed using -the option ``-I`` `path` (in the OCaml world, there is neither a +|OCaml| object files (``.cmo`` or ``.cmxs``) rather than |Coq| object +files as described above. The |OCaml| loadpath is managed using +the option ``-I`` `path` (in the |OCaml| world, there is neither a notion of logical name prefix nor a way to access files in subdirectories of path). See the command :cmd:`Declare ML Module` in -:ref:`compiled-files` to understand the need of the OCaml loadpath. +:ref:`compiled-files` to understand the need of the |OCaml| loadpath. See :ref:`command-line-options` for a more general view over the |Coq| command line options. diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 48647deeff..17f569ca2a 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -45,13 +45,13 @@ applications of these primitive operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Uint63` module. Said OCaml module is not produced by +module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types +and functions of a :g:`Uint63` module. That |OCaml| module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq. +can be taken from the kernel of |Coq|. -Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +Literal values (at type :g:`Int63.int`) are extracted to literal |OCaml| values wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the function :g:`Uint63.compile` from the kernel). @@ -94,13 +94,13 @@ to comply with the IEEE 754 standard for floating-point arithmetic. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Float64` module. Said OCaml module is not produced by +module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types +and functions of a :g:`Float64` module. Said |OCaml| module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq. +can be taken from the kernel of |Coq|. -Literal values (of type :g:`Float64.t`) are extracted to literal OCaml +Literal values (of type :g:`Float64.t`) are extracted to literal |OCaml| values (of type :g:`float`) written in hexadecimal notation and wrapped into the :g:`Float64.of_float` constructor, e.g.: :g:`Float64.of_float (0x1p+0)`. @@ -144,19 +144,19 @@ operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Parray` module. Said OCaml module is not produced by +module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types +and functions of a :g:`Parray` module. Said |OCaml| module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq (see ``kernel/parray.ml``). +can be taken from the kernel of |Coq| (see ``kernel/parray.ml``). -Coq's primitive arrays are persistent data structures. Semantically, a set operation +|Coq|'s primitive arrays are persistent data structures. Semantically, a set operation ``t.[i <- a]`` represents a new array that has the same values as ``t``, except at position ``i`` where its value is ``a``. The array ``t`` still exists, can still be used and its values were not modified. Operationally, the implementation -of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not +of |Coq|'s primitive arrays is optimized so that the new array ``t.[i <- a]`` does not copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`. -In short, the implementation keeps one version of ``t`` as an OCaml native array and +In short, the implementation keeps one version of ``t`` as an |OCaml| native array and other versions as lists of modifications to ``t``. Accesses to the native array version are constant time operations. However, accesses to versions where all the cells of the array are modified have O(n) access time, the same as a list. The version that is kept as the native array diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index b2099b8636..e6df3ee9f5 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -18,7 +18,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. insertprodn record_definition field_def .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations } + record_definition ::= {? > } @ident_decl {* @binder } {? : @sort } {? := {? @ident } %{ {*; @record_field } {? ; } %} } record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term @@ -26,19 +26,28 @@ expressions. In this sense, the :cmd:`Record` construction allows defining term_record ::= %{%| {*; @field_def } {? ; } %|%} field_def ::= @qualid {* @binder } := @term - Each :n:`@record_definition` defines a record named by :n:`@ident_decl`. The constructor name is given by :n:`@ident`. If the constructor name is not specified, then the default name :n:`Build_@ident` is used, where :n:`@ident` is the record name. - If :n:`@type` is - omitted, the default type is :math:`\Type`. The identifiers inside the brackets are the field names. - The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`. + If :token:`sort` is omitted, the default sort is Type. Notice that the type of an identifier can depend on a previously-given identifier. Thus the order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole or to individual fields. + .. todo + "Record foo2:Prop := { a }." gives the error "Cannot infer this placeholder of type "Type", + while "Record foo2:Prop := { a:Type }." gives the output "foo2 is defined. + a cannot be defined because it is informative and foo2 is not." + Your thoughts? + + :n:`{? > }` + If provided, the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). See :ref:`coercions`. + Notations can be attached to fields using the :n:`@decl_notations` annotation. :cmd:`Record` and :cmd:`Structure` are synonyms. @@ -76,7 +85,7 @@ Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: :n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`. -To build an object of type :token:`ident`, one should provide the constructor +To build an object of type :token:`ident`, provide the constructor :n:`@ident__0` with the appropriate number of terms filling the fields of the record. .. example:: diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index df50dbafe3..c70f7a347b 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -84,7 +84,7 @@ Sections create local contexts which can be shared across multiple definitions. will be wrapped with a :n:`@term_let` with the same declaration. As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, - if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + if :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 2904250e41..645986be9c 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -29,6 +29,7 @@ Private (matching) inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. attr:: private(matching) + :name: private(matching); Private This attribute can be used to forbid the use of the :g:`match` construct on objects of this inductive type outside of the module diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 0ae9fab7ab..29877e1b32 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -377,7 +377,7 @@ Effects of :cmd:`Arguments` on unfolding Bidirectionality hints ~~~~~~~~~~~~~~~~~~~~~~ -When type-checking an application, Coq normally does not use information from +When type-checking an application, |Coq| normally does not use information from the context to infer the types of the arguments. It only checks after the fact that the type inferred for the application is coherent with the expected type. Bidirectionality hints make it possible to specify that after type-checking the @@ -394,7 +394,7 @@ the context to help inferring the types of the remaining arguments. * *type inference*, with is inferring the type of a construct by analyzing the construct. Methods that combine these approaches are known as *bidirectional typing*. - Coq normally uses only the first approach to infer the types of arguments, + |Coq| normally uses only the first approach to infer the types of arguments, then later verifies that the inferred type is consistent with the expected type. *Bidirectionality hints* specify to use both methods: after type checking the first arguments of an application (appearing before the `&` in :cmd:`Arguments`), @@ -416,7 +416,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`). Definition b2n (b : bool) := if b then 1 else 0. Coercion b2n : bool >-> nat. - Coq cannot automatically coerce existential statements over ``bool`` to + |Coq| cannot automatically coerce existential statements over ``bool`` to statements over ``nat``, because the need for inserting a coercion is known only from the expected type of a subterm: @@ -431,7 +431,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`). Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). -Coq will attempt to produce a term which uses the arguments you +|Coq| will attempt to produce a term which uses the arguments you provided, but in some cases involving Program mode the arguments after the bidirectionality starts may be replaced by convertible but syntactically different terms. diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index bfda8befff..38c9fa336d 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -159,7 +159,7 @@ of the terms that are compared. End theory. End EQ. -We use Coq modules as namespaces. This allows us to follow the same +We use |Coq| modules as namespaces. This allows us to follow the same pattern and naming convention for the rest of the chapter. The base namespace contains the definitions of the algebraic structure. To keep the example small, the algebraic structure ``EQ.type`` we are @@ -224,7 +224,7 @@ example work: Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). The error message is telling that |Coq| has no idea on how to compare -pairs of objects. The following construction is telling Coq exactly +pairs of objects. The following construction is telling |Coq| exactly how to do that. .. coqtop:: all diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 20f4310d13..dc208a63a0 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -68,7 +68,7 @@ Inferable subterms ~~~~~~~~~~~~~~~~~~ Expressions often contain redundant pieces of information. Subterms that can be -automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will +automatically inferred by |Coq| can be replaced by the symbol ``_`` and |Coq| will guess the missing piece of information. .. extracted from Gallina extensions chapter diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index f8375e93ce..9457505feb 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -115,7 +115,7 @@ application will include that argument. Otherwise, the argument is *non-maximally inserted* and the partial application will not include that argument. Each implicit argument can be declared to be inserted maximally or non -maximally. In Coq, maximally inserted implicit arguments are written between curly braces +maximally. In |Coq|, maximally inserted implicit arguments are written between curly braces "{ }" and non-maximally inserted implicit arguments are written in square brackets "[ ]". .. seealso:: :flag:`Maximal Implicit Insertion` diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst index ed207ca743..ea7271179e 100644 --- a/doc/sphinx/language/extensions/index.rst +++ b/doc/sphinx/language/extensions/index.rst @@ -4,7 +4,7 @@ Language extensions =================== -Elaboration extends the language accepted by the Coq kernel to make it +Elaboration extends the language accepted by the |Coq| kernel to make it easier to use. For example, this lets the user omit most type annotations because they can be inferred, call functions with implicit arguments which will be inferred as well, extend the syntax with diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index c36b9deef3..3c1983ee97 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -290,6 +290,43 @@ This example emphasizes what the printing settings offer. Print snd. +Conventions about unused pattern-matching variables +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern-matching variables that are not used on the right-hand side of ``=>`` are +considered the sign of a potential error. For instance, it could +result from an undetected mispelled constant constructor. By default, +a warning is issued in such situations. + +.. warn:: Unused variable @ident catches more than one case. + + This indicates that an unused pattern variable :token:`ident` + occurs in a pattern-matching clause used to complete at least two + cases of the pattern-matching problem. + + The warning can be deactivated by using a variable name starting + with ``_`` or by setting ``Set Warnings + "-unused-pattern-matching-variable"``. + + Here is an example where the warning is activated. + + .. example:: + + .. coqtop:: none + + Set Warnings "-unused-pattern-matching-variable". + + .. coqtop:: all + + Definition is_zero (o : option nat) := match o with + | Some 0 => true + | x => false + end. + + .. coqtop:: none + + Set Warnings "+unused-pattern-matching-variable". + Patterns -------- @@ -639,7 +676,7 @@ Dependent pattern matching ~~~~~~~~~~~~~~~~~~~~~~~~~~ The examples given so far do not need an explicit elimination -predicate because all the |rhs| have the same type and Coq +predicate because all the |rhs| have the same type and |Coq| succeeds to synthesize it. Unfortunately when dealing with dependent patterns it often happens that we need to write cases where the types of the |rhs| are different instances of the elimination predicate. The |