diff options
Diffstat (limited to 'doc/sphinx/language/gallina-extensions.rst')
-rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 72 |
1 files changed, 32 insertions, 40 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 1a57e5419..c21d8d4ec 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1925,69 +1925,61 @@ 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|. - -Canonical structures are particularly useful when mixed with coercions -and strict implicit arguments. - -.. example:: - - Here is an example. + This command declares :token:`qualid` as a canonical structure. - .. coqtop:: all + 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|. - Require Import Relations. + Canonical structures are particularly useful when mixed with coercions + and strict implicit arguments. - Require Import EqNat. + .. example:: - Set Implicit Arguments. + Here is an example. - Unset Strict Implicit. + .. coqtop:: all - Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; - Prf_equiv : equivalence Carrier Equal}. + Require Import Relations. - Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). + Require Import EqNat. - Axiom eq_nat_equiv : equivalence nat eq_nat. + Set Implicit Arguments. - Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. + Unset Strict Implicit. - Canonical Structure nat_setoid. + Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; + Prf_equiv : equivalence Carrier Equal}. -Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A`` -and ``B`` can be synthesized in the next statement. + Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). -.. coqtop:: all + Axiom eq_nat_equiv : equivalence nat eq_nat. - Lemma is_law_S : is_law S. + Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. -Remark: If a same field occurs in several canonical structure, then -only the structure declared first as canonical is considered. + Canonical Structure nat_setoid. -.. cmdv:: Canonical Structure @ident := @term : @type + 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 + .. coqtop:: all -.. cmdv:: Canonical Structure @ident : @type := @term + Lemma is_law_S : is_law S. -These are equivalent to a regular definition of `ident` followed by the declaration -``Canonical Structure`` `ident`. + .. note:: + If a same field occurs in several canonical structures, then + only the structure declared first as canonical is considered. -See also: more examples in user contribution category (Rocq/ALGEBRA). + .. cmdv:: Canonical Structure @ident {? : @type } := @term + This is equivalent to a regular definition of :token:`ident` followed by the + declaration :n:`Canonical Structure @ident`. -Printing Canonical Projections -++++++++++++++++++++++++++++++ .. cmd:: Print Canonical Projections |