diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-13 15:21:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-13 15:21:31 -0400 |
| commit | 59d38e35dcac862305678a1010511ae676d68ddc (patch) | |
| tree | e8b34304af01246418ca9629e660394b2f979ffe /src/Util/Decidable.v | |
| parent | 9fecab22475367b8b78946721da15e0aa7f13245 (diff) | |
Add dec_eq_comparison
Diffstat (limited to 'src/Util/Decidable.v')
| -rw-r--r-- | src/Util/Decidable.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index e5f9cf0bd..014af738f 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -93,6 +93,7 @@ Global Instance dec_eq_list {A} `{DecidableRel (@eq A)} : DecidableRel (@eq (lis Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)) | 10. exact _. Defined. Global Instance dec_eq_sigT_hprop {A P} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sigT A P)) | 10. exact _. Defined. Global Instance dec_eq_sig_hprop {A} {P : A -> Prop} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sig A P)) | 10. exact _. Defined. +Global Instance dec_eq_comparison : DecidableRel (@eq comparison) | 10. exact _. Defined. Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined. Global Instance dec_le_nat : DecidableRel le := Compare_dec.le_dec. |