diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-31 15:24:52 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-31 15:24:52 +0000 |
| commit | 67e9cef251a291fab7f656f3dd0b9f2c0bde5a59 (patch) | |
| tree | ae8aab8faa2b3c6998fffa0cade9766d01160789 /theories/Classes/SetoidClass.v | |
| parent | 7f99d8016ced351efd0a42598a9d18001b2e4d46 (diff) | |
Debug implementation of dependent induction/dependent destruction and document it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidClass.v')
| -rw-r--r-- | theories/Classes/SetoidClass.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index c5befaa11..f61b4a415 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -223,17 +223,21 @@ Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => (** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *) -Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] (m : a -> b -> c) : Prop := +Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] + (m : a -> b -> c) : Prop := forall x y, eqa x y -> forall z w, eqb z w -> eqc (m x z) (m y w). -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => BinaryMorphism (m : a -> b -> c) := +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => + BinaryMorphism (m : a -> b -> c) := respect2 : binary_respectful m. -Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] (m : a -> b -> c -> d) : Prop := +Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] + (m : a -> b -> c -> d) : Prop := forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v). -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => TernaryMorphism (m : a -> b -> c -> d) := +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => + TernaryMorphism (m : a -> b -> c -> d) := respect3 : ternary_respectful m. (** Definition of the usual morphisms in [Prop]. *) |