diff options
Diffstat (limited to 'theories/Classes/Equivalence.v')
| -rw-r--r-- | theories/Classes/Equivalence.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index d7774a2d7..f40d2e2a5 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -37,23 +37,25 @@ Definition equiv [ Equivalence A R ] : relation A := R. Typeclasses unfold @equiv. + + (* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *) -(* Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. *) +Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. -(* Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. *) +Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. -(* Next Obligation. *) -(* Proof. *) -(* symmetry ; auto. *) -(* Qed. *) + Next Obligation. + Proof. + symmetry ; auto. + Qed. -(* Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. *) +Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. -(* Next Obligation. *) -(* Proof. *) -(* transitivity y ; auto. *) -(* Qed. *) + Next Obligation. + Proof. + transitivity y ; auto. + Qed. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) |