diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-27 11:44:39 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-27 11:44:39 -0700 |
| commit | 27aa3a1e358ca9281721e3a3f4137979d16aab7e (patch) | |
| tree | 045ecc481cf07b67f52d2de00d2dfbf4e720566e /src/Util/Sum.v | |
| parent | c5626e9e937246b9163067dc4a88ee09c4164136 (diff) | |
Add decidable instances for sumwise and fieldwise
Diffstat (limited to 'src/Util/Sum.v')
| -rw-r--r-- | src/Util/Sum.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/Sum.v b/src/Util/Sum.v index 915f58df9..1ee8ea69a 100644 --- a/src/Util/Sum.v +++ b/src/Util/Sum.v @@ -1,5 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. +Require Import Crypto.Util.Decidable. Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B) := fun x y => match x, y with @@ -25,3 +26,9 @@ Ltac congruence_sum_step := | [ H : inr _ = inr _ |- _ ] => inversion H; clear H end. Ltac congruence_sum := repeat congruence_sum_step. + +Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances. +Global Instance dec_sumwise {A B RA RB} {HA : DecidableRel RA} {HB : DecidableRel RB} : DecidableRel (@sumwise A B RA RB) | 10. +Proof. + intros [x|x] [y|y]; exact _. +Qed. |