diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 2 |
3 files changed, 12 insertions, 11 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index dd21ea09bd..b593b0cef1 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. Arguments Mixin {e le} _. @@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we are adding to ``EQ`` and ``LE``. In particular it contains the requirement that the two relations we are combining are compatible. +The `class_of` projection of the `type` structure is annotated as *not canonical*; +it plays no role in the search for instances. + Unfortunately there is still an obstacle to developing the algebraic theory of this new class. @@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. FIXME shouldn't warn - -.. coqtop:: all warn +.. coqtop:: all Module Add_instance_attempt. @@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. FIXME should not warn - -.. coqtop:: all warn +.. coqtop:: all Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index c0c8c2d79c..8935ba27e3 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -10,9 +10,9 @@ SProp (proof irrelevant propositions) This section describes the extension of |Coq| with definitionally proof irrelevant propositions (types in the sort :math:`\SProp`, also known as strict propositions). To use :math:`\SProp` you must pass -``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`. +``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`. -.. opt:: Allow StrictProp +.. flag:: Allow StrictProp :name: Allow StrictProp Allows using :math:`\SProp` when set and forbids it when unset. The @@ -201,10 +201,10 @@ This means that some errors will be delayed until ``Qed``: Abort. -.. opt:: Elaboration StrictProp Cumulativity +.. flag:: Elaboration StrictProp Cumulativity :name: Elaboration StrictProp Cumulativity - Unset this option (it's on by default) to be strict with regard to + Unset this flag (it is on by default) to be strict with regard to :math:`\SProp` cumulativity during elaboration. The implementation of proof irrelevance uses inferred "relevance" diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index a5e9023732..77a6ee79cc 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -405,6 +405,8 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + When considering local hypotheses, we use the union of all the modes + declared in the given databases. .. cmdv:: typeclasses eauto @num |