diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 33 |
4 files changed, 22 insertions, 27 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3e414a714c..a9d894cab5 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -313,7 +313,9 @@ 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. -.. coqtop:: all +.. FIXME shouldn't warn + +.. coqtop:: all warn Module Add_instance_attempt. @@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. FIXME should not warn + +.. coqtop:: all warn Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index d77690458d..3ec6c118af 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -295,7 +295,7 @@ By default, implicit arguments are omitted in patterns. So we write: end). But the possibility to use all the arguments is given by “``@``” implicit -explicitations (as for terms 2.7.11). +explicitations (as for terms, see :ref:`explicit-applications`). .. coqtop:: all diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index cc788b3595..b474c51f17 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -627,14 +627,10 @@ logical equivalence: Instance all_iff_morphism (A : Type) : Proper (pointwise_relation A iff ==> iff) (@all A). -.. coqtop:: all +.. coqtop:: all abort Proof. simpl_relation. -.. coqtop:: none - - Abort. - One then has to show that if two predicates are equivalent at every point, their universal quantifications are equivalent. Once we have declared such a morphism, it will be used by the setoid rewriting diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 43d302114e..c7ea7e326f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -44,25 +44,20 @@ Leibniz equality on some type. An example implementation is: eqb_leibniz x y H := match x, y return x = y with tt, tt => eq_refl tt end }. -If one does not give all the members in the Instance declaration, Coq -enters the proof-mode and the user is asked to build inhabitants of -the remaining fields, e.g.: +Using :cmd:`Program Instance`, if one does not give all the members in +the Instance declaration, Coq generates obligations for the remaining +fields, e.g.: .. coqtop:: in - Instance eq_bool : EqDec bool := + Require Import Program.Tactics. + Program Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }. .. coqtop:: all - Proof. intros x y H. - -.. coqtop:: all - - destruct x ; destruct y ; (discriminate || reflexivity). - -.. coqtop:: all - + Next Obligation. + destruct x ; destruct y ; (discriminate || reflexivity). Defined. One has to take care that the transparency of every field is @@ -131,14 +126,14 @@ the constraints as a binding context before the instance, e.g.: .. coqtop:: in - Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := + Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) end }. .. coqtop:: none - Abort. + Admit Obligations. These instances are used just as well as lemmas in the instance hint database. @@ -157,13 +152,13 @@ vernacular, except it accepts any binding context as argument. For example: Context `{EA : EqDec A}. - Global Instance option_eqb : EqDec (option A) := + Global Program Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true | _, _ => false end }. - Admitted. + Admit Obligations. End EqDec_defs. @@ -564,12 +559,12 @@ Settings This flag allows to switch the behavior of instance declarations made through the Instance command. - + When it is on (the default), instances that have unsolved holes in + + When it is off (the default), they fail with an error instead. + + + When it is on, instances that have unsolved holes in their proof-term silently open the proof mode with the remaining obligations to prove. - + When it is off, they fail with an error instead. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ |