From 27aa3a1e358ca9281721e3a3f4137979d16aab7e Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 27 Jun 2016 11:44:39 -0700
Subject: Add decidable instances for sumwise and fieldwise

---
 src/Util/Sum.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/Util/Sum.v')

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.
-- 
cgit v1.2.3