diff options
Diffstat (limited to 'theories/Classes/CRelationClasses.v')
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index bc821532fe..bb873588b1 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -177,6 +177,7 @@ Section Defs. a rewrite crelation. *) Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA. + Defined. (** Leibniz equality. *) Section Leibniz. @@ -195,7 +196,10 @@ End Defs. (** Default rewrite crelations handled by [setoid_rewrite]. *) Instance: RewriteRelation impl. +Defined. + Instance: RewriteRelation iff. +Defined. (** Hints to drive the typeclass resolution avoiding loops due to the use of full unification. *) @@ -299,7 +303,8 @@ Section Binary. fun R R' => forall x y, iffT (R x y) (R' x y). Global Instance: RewriteRelation relation_equivalence. - + Defined. + Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A := fun x y => prod (R x y) (R' x y). |