diff options
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 6802a86c3..d08c52c82 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -1,5 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. +Require Import Crypto.Util.Decidable. Fixpoint tuple' T n : Type := match n with @@ -79,3 +80,17 @@ Qed. Arguments fieldwise' {A B n} _ _ _. Arguments fieldwise {A B n} _ _ _. + +Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances. +Global Instance dec_fieldwise' {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise' A A n RA) | 10. +Proof. + induction n; simpl @fieldwise'. + { exact _. } + { intros ??. + exact _. } +Qed. + +Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise A A n RA) | 10. +Proof. + destruct n; unfold fieldwise; exact _. +Qed. |