diff options
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/Setoid.tex | 10 | ||||
-rw-r--r-- | doc/stdlib/index-list.html.template | 4 |
2 files changed, 11 insertions, 3 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index d2b6d1151..ba847562e 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -623,10 +623,13 @@ Reset Initial. Require Import Setoid. \end{coq_eval} \begin{coq_example} -Instance {A : Type} => all_iff_morphism : +Instance all_iff_morphism (A : Type) : Morphism (pointwise_relation iff ==> iff) (@all A). Proof. simpl_relation. \end{coq_example} +\begin{coq_eval} +Admitted. +\end{coq_eval} One then has to show that if two predicates are equivalent at every point, their universal quantifications are equivalent. Once we have @@ -653,12 +656,13 @@ Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) := forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l'). \end{coq_eval} \begin{coq_example*} -Instance [ Equivalence A eqA, Equivalence B eqB ] => +Instance map_morphism [ Equivalence A eqA, Equivalence B eqB ] : Morphism ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). \end{coq_example*} -where \texttt{list\_equiv} implements an equivalence on lists. +where \texttt{list\_equiv} implements an equivalence on lists +parameterized by an equivalence on the elements. Note that when one does rewriting with a lemma under a binder using \texttt{setoid\_rewrite}, the application of the lemma may capture diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index c86338175..48dbb3f01 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -438,12 +438,16 @@ through the <tt>Require Import</tt> command.</p> Support for dependently-typed programming. </dt> <dd> + theories/Program/Basics.v theories/Program/Wf.v + theories/Program/Subset.v theories/Program/Equality.v theories/Program/Tactics.v theories/Program/Utils.v + theories/Program/Syntax.v theories/Program/Program.v theories/Program/FunctionalExtensionality.v + theories/Program/Combinators.v </dd> </dl> |