diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-18 20:54:49 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-18 20:54:49 -0400 |
| commit | 502ddd692460ca2d1b0432bc215616615cd0dcd6 (patch) | |
| tree | 8325fd77cf5cf833b9c966a985421924650b10a0 /src/Util/Decidable.v | |
| parent | 00af576224d267cafd149ee32f28e18dd4f9b45f (diff) | |
Add dec eq for option, list
Diffstat (limited to 'src/Util/Decidable.v')
| -rw-r--r-- | src/Util/Decidable.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index cb47a3625..6030ae819 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -91,6 +91,8 @@ Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined. Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined. Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined. Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)) | 10. exact _. Defined. +Global Instance dec_eq_option {A} `{DecidableRel (@eq A)} : DecidableRel (@eq (option A)) | 10. exact _. Defined. +Global Instance dec_eq_list {A} `{DecidableRel (@eq A)} : DecidableRel (@eq (list A)) | 10. exact _. Defined. 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. |