aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-16 18:12:48 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-16 18:12:48 +0200
commitcee11fc609cb7d7087adabba389a97991e636219 (patch)
tree730198a5931669aca5645c81f2f58bcc25b8d2f8
parentf2e2d1d9f00ab731bd2bbe1dd57d685ac5024204 (diff)
parent8c64c9e2479fe12634a22b4c90da12a24833e9bc (diff)
Merge PR #7814: doc: Add "Print Canonical Projections" command to Command index
-rw-r--r--doc/sphinx/language/gallina-extensions.rst83
1 files changed, 42 insertions, 41 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ff5d352c9..c21d8d4ec 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1925,74 +1925,75 @@ applied to an unknown structure instance (an implicit argument) and a
value. The complete documentation of canonical structures can be found
in :ref:`canonicalstructures`; here only a simple example is given.
-Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the
-structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that
-`qualid` is declared as a canonical structure using the command
-
.. cmd:: Canonical Structure @qualid
-Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
-solved during the type-checking process, `qualid` is used as a solution.
-Otherwise said, `qualid` is canonically used to extend the field |c_i|
-into a complete structure built on |c_i|.
+ This command declares :token:`qualid` as a canonical structure.
-Canonical structures are particularly useful when mixed with coercions
-and strict implicit arguments. Here is an example.
+ Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
+ structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
+ Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
+ solved during the type-checking process, :token:`qualid` is used as a solution.
+ Otherwise said, :token:`qualid` is canonically used to extend the field |c_i|
+ into a complete structure built on |c_i|.
-.. coqtop:: all
+ Canonical structures are particularly useful when mixed with coercions
+ and strict implicit arguments.
- Require Import Relations.
+ .. example::
- Require Import EqNat.
+ Here is an example.
- Set Implicit Arguments.
+ .. coqtop:: all
- Unset Strict Implicit.
+ Require Import Relations.
- Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
- Prf_equiv : equivalence Carrier Equal}.
+ Require Import EqNat.
- Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
+ Set Implicit Arguments.
- Axiom eq_nat_equiv : equivalence nat eq_nat.
+ Unset Strict Implicit.
- Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
+ Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
+ Prf_equiv : equivalence Carrier Equal}.
- Canonical Structure nat_setoid.
+ Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
-Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A``
-and ``B`` can be synthesized in the next statement.
+ Axiom eq_nat_equiv : equivalence nat eq_nat.
-.. coqtop:: all
+ Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
- Lemma is_law_S : is_law S.
+ Canonical Structure nat_setoid.
-Remark: If a same field occurs in several canonical structure, then
-only the structure declared first as canonical is considered.
+ Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A`
+ and :g:`B` can be synthesized in the next statement.
-.. cmdv:: Canonical Structure @ident := @term : @type
+ .. coqtop:: all
-.. cmdv:: Canonical Structure @ident := @term
+ Lemma is_law_S : is_law S.
-.. cmdv:: Canonical Structure @ident : @type := @term
+ .. note::
+ If a same field occurs in several canonical structures, then
+ only the structure declared first as canonical is considered.
-These are equivalent to a regular definition of `ident` followed by the declaration
-``Canonical Structure`` `ident`.
+ .. cmdv:: Canonical Structure @ident {? : @type } := @term
-See also: more examples in user contribution category (Rocq/ALGEBRA).
+ This is equivalent to a regular definition of :token:`ident` followed by the
+ declaration :n:`Canonical Structure @ident`.
-Print Canonical Projections.
-++++++++++++++++++++++++++++
+.. cmd:: Print Canonical Projections
-This displays the list of global names that are components of some
-canonical structure. For each of them, the canonical structure of
-which it is a projection is indicated. For instance, the above example
-gives the following output:
+ This displays the list of global names that are components of some
+ canonical structure. For each of them, the canonical structure of
+ which it is a projection is indicated.
-.. coqtop:: all
+ .. example::
+
+ For instance, the above example gives the following output:
+
+ .. coqtop:: all
- Print Canonical Projections.
+ Print Canonical Projections.
Implicit types of variables