diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-12 17:55:10 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-12 18:12:24 +0200 |
| commit | 1f3ea50258490ac8b5a395ac0ff2bca7326e755f (patch) | |
| tree | 2fda4c14c0aee11501be7261d177c269f7029391 /theories/Classes | |
| parent | f480f07c232b4bcc4ea67bf0577e267d0fdc35f4 (diff) | |
Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1a40e5d59..15cb02d37 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -89,6 +89,11 @@ Section Defs. Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 := { }. + (** An Equivalence is a PreOrder plus symmetry. *) + + Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 := + { }. + (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) := |