aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r--doc/sphinx/language/cic.rst2
-rw-r--r--doc/sphinx/language/coq-library.rst48
-rw-r--r--doc/sphinx/language/core/assumptions.rst4
-rw-r--r--doc/sphinx/language/core/basic.rst44
-rw-r--r--doc/sphinx/language/core/conversion.rst10
-rw-r--r--doc/sphinx/language/core/modules.rst2
-rw-r--r--doc/sphinx/language/core/primitive.rst19
-rw-r--r--doc/sphinx/language/core/records.rst2
-rw-r--r--doc/sphinx/language/core/sorts.rst2
-rw-r--r--doc/sphinx/language/core/variants.rst19
-rw-r--r--doc/sphinx/language/extensions/evars.rst32
-rw-r--r--doc/sphinx/language/extensions/implicit-arguments.rst6
-rw-r--r--doc/sphinx/language/extensions/match.rst18
13 files changed, 126 insertions, 82 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 768c83150e..f1ed64e52a 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -274,7 +274,7 @@ following rules.
.. inference:: Prod-Type
\WTEG{T}{s}
- s \in \{\SProp, \Type{i}\}
+ s \in \{\SProp, \Type(i)\}
\WTE{\Gamma::(x:T)}{U}{\Type(i)}
--------------------------------
\WTEG{∀ x:T,~U}{\Type(i)}
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index f9d24fde0e..485dfd964d 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -40,7 +40,7 @@ in the |Coq| root directory; this includes the modules
``Datatypes``,
``Specif``,
``Peano``,
-``Wf`` and
+``Wf`` and
``Tactics``.
Module ``Logic_Type`` also makes it in the initial state.
@@ -175,7 +175,7 @@ Quantifiers
Then we find first-order quantifiers:
.. coqtop:: in
-
+
Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
Inductive ex (A: Set) (P:A -> Prop) : Prop :=
ex_intro (x:A) (_:P x).
@@ -256,12 +256,12 @@ Finally, a few easy lemmas are provided.
single: f_equal2 ... f_equal5 (term)
The theorem ``f_equal`` is extended to functions with two to five
-arguments. The theorem are names ``f_equal2``, ``f_equal3``,
+arguments. The theorem are names ``f_equal2``, ``f_equal3``,
``f_equal4`` and ``f_equal5``.
For instance ``f_equal3`` is defined the following way.
.. coqtop:: in abort
-
+
Theorem f_equal3 :
forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
(x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
@@ -324,7 +324,7 @@ Programming
Note that zero is the letter ``O``, and *not* the numeral ``0``.
-The predicate ``identity`` is logically
+The predicate ``identity`` is logically
equivalent to equality but it lives in sort ``Type``.
It is mainly maintained for compatibility.
@@ -367,7 +367,7 @@ infix notation ``||``), ``xorb``, ``implb`` and ``negb``.
Specification
~~~~~~~~~~~~~
-The following notions defined in module ``Specif.v`` allow to build new data-types and specifications.
+The following notions defined in module ``Specif.v`` allow to build new data-types and specifications.
They are available with the syntax shown in the previous section :ref:`datatypes`.
For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct
@@ -393,11 +393,11 @@ provided.
.. coqtop:: in
Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
- Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
+ Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
exist2 (x:A) (_:P x) (_:Q x).
A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined,
-when the predicate ``P`` is now defined as a
+when the predicate ``P`` is now defined as a
constructor of types in ``Type``.
.. index::
@@ -556,7 +556,7 @@ section :tacn:`refine`). This scope is opened by default.
Now comes the content of module ``Peano``:
.. coqdoc::
-
+
Theorem eq_S : forall x y:nat, x = y -> S x = S y.
Definition pred (n:nat) : nat :=
match n with
@@ -628,7 +628,7 @@ induction principle.
.. coqdoc::
Theorem nat_case :
- forall (n:nat) (P:nat -> Prop),
+ forall (n:nat) (P:nat -> Prop),
P 0 -> (forall m:nat, P (S m)) -> P n.
Theorem nat_double_ind :
forall R:nat -> nat -> Prop,
@@ -640,7 +640,7 @@ induction principle.
Well-founded recursion
~~~~~~~~~~~~~~~~~~~~~~
-The basic library contains the basics of well-founded recursion and
+The basic library contains the basics of well-founded recursion and
well-founded induction, in module ``Wf.v``.
.. index::
@@ -669,7 +669,7 @@ well-founded induction, in module ``Wf.v``.
forall P:A -> Prop,
(forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
-The automatically generated scheme ``Acc_rect``
+The automatically generated scheme ``Acc_rect``
can be used to define functions by fixpoints using
well-founded relations to justify termination. Assuming
extensionality of the functional used for the recursive call, the
@@ -677,7 +677,7 @@ fixpoint equation can be proved.
.. index::
single: Fix_F (term)
- single: fix_eq (term)
+ single: Fix_eq (term)
single: Fix_F_inv (term)
single: Fix_F_eq (term)
@@ -696,7 +696,7 @@ fixpoint equation can be proved.
forall (x:A) (r:Acc x),
F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
- Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
+ Lemma Fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
End FixPoint.
End Well_founded.
@@ -741,7 +741,7 @@ The standard library
Survey
~~~~~~
-The rest of the standard library is structured into the following
+The rest of the standard library is structured into the following
subdirectories:
* **Logic** : Classical logic and dependent equality
@@ -751,8 +751,8 @@ subdirectories:
* **ZArith** : Basic relative integer arithmetic
* **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words)
* **Bool** : Booleans (basic functions and results)
- * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types)
- * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.)
+ * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types)
+ * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.)
* **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees)
* **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...)
* **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format)
@@ -903,7 +903,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
.. tacn:: discrR
:name: discrR
-
+
Proves that two real integer constants are different.
.. example::
@@ -931,7 +931,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
.. tacn:: split_Rmult
:name: split_Rmult
-
+
Splits a condition that a product is non null into subgoals
corresponding to the condition on each operand of the product.
@@ -963,7 +963,7 @@ List library
single: fold_left (term)
single: fold_right (term)
-Some elementary operations on polymorphic lists are defined here.
+Some elementary operations on polymorphic lists are defined here.
They can be accessed by requiring module ``List``.
It defines the following notions:
@@ -1052,9 +1052,9 @@ Notation Interpretation
``_ + _`` ``add``
``_ * _`` ``mul``
``_ / _`` ``div``
-``_ == _`` ``eqb``
-``_ < _`` ``ltb``
-``_ <= _`` ``leb``
+``_ =? _`` ``eqb``
+``_ <? _`` ``ltb``
+``_ <=? _`` ``leb``
``_ ?= _`` ``compare``
=========== ==============
@@ -1062,7 +1062,7 @@ Floating-point constants are parsed and pretty-printed as (17-digit)
decimal constants. This ensures that the composition
:math:`\text{parse} \circ \text{print}` amounts to the identity.
-.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing]
+.. warn:: The constant @number is not a binary64 floating-point value. A closest value @number will be used and unambiguously printed @number. [inexact-float,parsing]
Not all decimal constants are floating-point values. This warning
is generated when parsing such a constant (for instance ``0.1``).
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 955f48b772..41e1c30f0d 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -125,7 +125,7 @@ has type :n:`@type`.
.. _Axiom:
-.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt }
+.. cmd:: @assumption_token {? Inline {? ( @natural ) } } {| {+ ( @assumpt ) } | @assumpt }
:name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables
.. insertprodn assumption_token of_type
@@ -138,7 +138,7 @@ has type :n:`@type`.
| {| Variable | Variables }
assumpt ::= {+ @ident_decl } @of_type
ident_decl ::= @ident {? @univ_decl }
- of_type ::= {| : | :> | :>> } @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
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 64b29c1c0b..45bdc019ac 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -111,33 +111,46 @@ Identifiers
symbols and non-breaking space. :production:`unicode_id_part`
non-exhaustively includes symbols for prime letters and subscripts.
-Numerals
- Numerals are sequences of digits with an optional fractional part
+Numbers
+ Numbers are sequences of digits with an optional fractional part
and exponent, optionally preceded by a minus sign. Hexadecimal numerals
- start with ``0x`` or ``0X``. :n:`@int` is an integer;
- a numeral without fractional nor exponent parts. :n:`@num` is a non-negative
- integer. Underscores embedded in the digits are ignored, for example
+ start with ``0x`` or ``0X``. :n:`@bigint` are integers;
+ numbers without fractional nor exponent parts. :n:`@bignat` are non-negative
+ integers. Underscores embedded in the digits are ignored, for example
``1_000_000`` is the same as ``1000000``.
- .. insertprodn numeral hexdigit
+ .. insertprodn number hexdigit
.. prodn::
- numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum }
- | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum }
- int ::= {? - } @num
- num ::= {| @decnum | @hexnum }
- decnum ::= @digit {* {| @digit | _ } }
+ number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat }
+ | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat }
+ integer ::= {? - } @natural
+ natural ::= @bignat
+ bigint ::= {? - } @bignat
+ bignat ::= {| @decnat | @hexnat }
+ decnat ::= @digit {* {| @digit | _ } }
digit ::= 0 .. 9
- hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
+ hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
hexdigit ::= {| 0 .. 9 | a .. f | A .. F }
- .. todo PR need some code fixes for hex, see PR 11948
+ :n:`@integer` and :n:`@natural` are limited to the range that fits
+ 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
+ :ref:`interpretations <notation-scopes>` for :n:`@number`. The
+ :cmd:`Number Notation` mechanism offers the user
+ a way to define custom parsers and printers for :n:`@number`.
Strings
Strings begin and end with ``"`` (double quote). Use ``""`` to represent
a double quote character within a string. In the grammar, strings are
identified with :production:`string`.
+ The :cmd:`String Notation` mechanism offers the
+ user a way to define custom parsers and printers for
+ :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`
@@ -227,6 +240,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
| @term_match
| @term_record
| @term_generalizing
+ | [| {*; @term } %| @term {? : @type } |] {? @univ_annot }
| @term_ltac
| ( @term )
qualid_annotated ::= @qualid {? @univ_annot }
@@ -291,7 +305,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
.. prodn::
document ::= {* @sentence }
sentence ::= {? @attributes } @command .
- | {? @attributes } {? @num : } @query_command .
+ | {? @attributes } {? @natural : } @query_command .
| {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... }
| @control_command
@@ -433,7 +447,7 @@ gray boxes after the labels "Flag", "Option" and "Table". In the pdf,
they appear after a boldface label. They are listed in the
:ref:`options_index`.
-.. cmd:: Set @setting_name {? {| @int | @string } }
+.. cmd:: Set @setting_name {? {| @integer | @string } }
:name: Set
If :n:`@setting_name` is a flag, no value may be provided; the flag
diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst
index 0f27b65107..6b031cfea3 100644
--- a/doc/sphinx/language/core/conversion.rst
+++ b/doc/sphinx/language/core/conversion.rst
@@ -5,8 +5,14 @@ Conversion rules
In |Cic|, there is an internal reduction mechanism. In particular, it
can decide if two programs are *intentionally* equal (one says
-*convertible*). Convertibility is described in this section.
+:term:`convertible`). Convertibility is described in this section.
+α-conversion
+~~~~~~~~~~~~
+
+Two terms are :gdef:`α-convertible <alpha-convertible>` if they are syntactically
+equal ignoring differences in the names of variables bound within the expression.
+For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`.
.. _beta-reduction:
@@ -153,7 +159,7 @@ relation :math:`t` reduces to :math:`u` in the global environment
reductions β, δ, ι or ζ.
We say that two terms :math:`t_1` and :math:`t_2` are
-*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the
+*βδιζη-convertible*, or simply :gdef:`convertible`, or *equivalent*, in the
global environment :math:`E` and local context :math:`Γ` iff there
exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
… \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 29e703c223..866104d5d1 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -67,7 +67,7 @@ together, as well as a means of massive abstraction.
module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl )
module_type_inl ::= ! @module_type
| @module_type {? @functor_app_annot }
- functor_app_annot ::= [ inline at level @num ]
+ functor_app_annot ::= [ inline at level @natural ]
| [ no inline ]
module_type ::= @qualid
| ( @module_type )
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index 727177b23a..48647deeff 100644
--- a/doc/sphinx/language/core/primitive.rst
+++ b/doc/sphinx/language/core/primitive.rst
@@ -133,7 +133,7 @@ follows:
Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
-The complete set of such operators can be obtained looking at the :g:`PArray` module.
+The rest of these operators can be found in the :g:`PArray` module.
These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
:g:`Print Assumptions` command.
@@ -150,7 +150,16 @@ 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``).
-Primitive arrays expose a functional interface, but they are internally
-implemented using a persistent data structure :cite:`ConchonFilliatre07wml`.
-Update and access to an element in the most recent copy of an array are
-constant time operations.
+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
+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
+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
+changes dynamically upon each get and set call: the current list of modifications
+is applied to the native array and the lists of modifications of the other versions
+are updated so that they still represent the same values.
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index 0080f1d052..cd44d06e67 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -19,7 +19,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
.. prodn::
record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations }
- record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
+ record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations }
field_body ::= {* @binder } @of_type
| {* @binder } @of_type := @term
| {* @binder } := @term
diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst
index 3517d70005..98dd9a5426 100644
--- a/doc/sphinx/language/core/sorts.rst
+++ b/doc/sphinx/language/core/sorts.rst
@@ -20,7 +20,7 @@ Sorts
| Type @%{ @universe %}
universe ::= max ( {+, @universe_expr } )
| @universe_expr
- universe_expr ::= @universe_name {? + @num }
+ universe_expr ::= @universe_name {? + @natural }
The types of types are called :gdef:`sorts <sort>`.
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index d00a2f4100..2904250e41 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -22,7 +22,7 @@ Variants
:attr:`universes(noncumulative)` and :attr:`private(matching)`
attributes.
- .. exn:: The @num th argument of @ident must be @ident in @type.
+ .. exn:: The @natural th argument of @ident must be @ident in @type.
:undocumented:
Private (matching) inductive types
@@ -57,6 +57,11 @@ Private (matching) inductive types
Definition by cases: match
--------------------------
+Objects of inductive types can be destructured by a case-analysis
+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.
+
.. insertprodn term_match pattern0
.. prodn::
@@ -74,13 +79,15 @@ Definition by cases: match
| %{%| {* @qualid := @pattern } %|%}
| _
| ( {+| @pattern } )
- | @numeral
+ | @number
| @string
-Objects of inductive types can be destructured by a case-analysis
-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.
+Note that the :n:`@pattern ::= @pattern10 : @term` production
+is not supported in :n:`match` patterns. Trying to use it will give this error:
+
+.. exn:: Casts are not supported in this pattern.
+ :undocumented:
+
This paragraph describes the basic form of pattern matching. See
Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index 40e0898871..20f4310d13 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -13,13 +13,13 @@ Existential variables
| ?[ ?@ident ]
| ?@ident {? @%{ {+; @ident := @term } %} }
-|Coq| terms can include existential variables which represents unknown
-subterms to eventually be replaced by actual subterms.
+|Coq| terms can include existential variables that represent unknown
+subterms that are eventually replaced with actual subterms.
-Existential variables are generated in place of unsolvable implicit
+Existential variables are generated in place of unsolved implicit
arguments or “_” placeholders when using commands such as ``Check`` (see
Section :ref:`requests-to-the-environment`) or when using tactics such as
-:tacn:`refine`, as well as in place of unsolvable instances when using
+:tacn:`refine`, as well as in place of unsolved instances when using
tactics such that :tacn:`eapply`. An existential
variable is defined in a context, which is the context of variables of
the placeholder which generated the existential variable, and a type,
@@ -43,22 +43,18 @@ existential variable is represented by “?” followed by an identifier.
Check identity _ (fun x => _).
In the general case, when an existential variable :n:`?@ident` appears
-outside of its context of definition, its instance, written under the
-form :n:`{ {*; @ident := @term} }` is appending to its name, indicating
+outside its context of definition, its instance, written in the
+form :n:`{ {*; @ident := @term} }`, is appended 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` flag
-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.
+Only the variables that are defined in another context are displayed:
+this is why an existential variable used in the same context as its
+context of definition is written with no instance.
+This behaviour may be changed: see :ref:`explicit-display-existentials`.
.. coqtop:: all
Check (fun x y => _) 0 1.
- Set Printing Existential Instances.
-
- Check (fun x y => _) 0 1.
-
Existential variables can be named by the user upon creation using
the syntax :n:`?[@ident]`. This is useful when the existential
variable needs to be explicitly handled later in the script (e.g.
@@ -88,6 +84,14 @@ Explicit displaying of existential instances for pretty-printing
context of an existential variable is instantiated at each of the
occurrences of the existential variable.
+.. coqtop:: all
+
+ Check (fun x y => _) 0 1.
+
+ Set Printing Existential Instances.
+
+ Check (fun x y => _) 0 1.
+
.. _tactics-in-terms:
Solving existential variables using tactics
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index bbd486e3ba..f8375e93ce 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -70,7 +70,7 @@ is said *contextual* if it can be inferred only from the knowledge of
the type of the context of the current expression. For instance, the
only argument of::
- nil : forall A:Set, list A`
+ nil : forall A:Set, list A
is contextual. Similarly, both arguments of a term of type::
@@ -217,7 +217,7 @@ usual implicit arguments disambiguation syntax.
The syntax is also supported in internal binders. For instance, in the
following kinds of expressions, the type of each declaration present
-in :token:`binders` can be bracketed to mark the declaration as
+in :n:`{* @binder }` can be bracketed to mark the declaration as
implicit:
* :n:`fun (@ident:forall {* @binder }, @type) => @term`,
* :n:`forall (@ident:forall {* @binder }, @type), @type`,
@@ -539,7 +539,7 @@ with free variables into a closed statement where these variables are
quantified explicitly. Use the :cmd:`Generalizable` command to designate
which variables should be generalized.
-It is activated for a binder by prefixing a \`, and for terms by
+It is activated within a binder by prefixing it with \`, and for terms by
surrounding it with \`{ }, or \`[ ] or \`( ).
Terms surrounded by \`{ } introduce their free variables as maximally
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index b4558ef07f..c36b9deef3 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -90,11 +90,15 @@ constructions. There are two variants of them.
First destructuring let syntax
++++++++++++++++++++++++++++++
+.. todo explain that this applies to all of the "let" constructs (Gallina, Ltac1 and Ltac2)
+ also add "irrefutable pattern" to the glossary
+ note that in Ltac2 an upper case ident is a constructor, lower case is a variable
+
The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1`
performs case analysis on :n:`@term__0` whose type must be an
inductive type with exactly one constructor. The number of variables
:n:`@ident__i` must correspond to the number of arguments of this
-contrustor. Then, in :n:`@term__1`, these variables are bound to the
+constructor. Then, in :n:`@term__1`, these variables are bound to the
arguments of the constructor in :n:`@term__0`. For instance, the
definition
@@ -875,19 +879,19 @@ generated expression and the original.
Here is a summary of the error messages corresponding to each
situation:
-.. exn:: The constructor @ident expects @num arguments.
+.. exn:: The constructor @ident expects @natural arguments.
+ The variable ident is bound several times in pattern term
+ Found a constructor of inductive type term while a constructor of term is expected
- The variable ident is bound several times in pattern termFound a constructor
- of inductive type term while a constructor of term is expectedPatterns are
- incorrect (because constructors are not applied to the correct number of the
+ Patterns are incorrect (because constructors are not applied to the correct number of
arguments, because they are not linear or they are wrongly typed).
.. exn:: Non exhaustive pattern matching.
The pattern matching is not exhaustive.
-.. exn:: The elimination predicate term should be of arity @num (for non \
- dependent case) or @num (for dependent case).
+.. exn:: The elimination predicate term should be of arity @natural (for non \
+ dependent case) or @natural (for dependent case).
The elimination predicate provided to match has not the expected arity.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:38:00 +0000