From c58855f90865aae024a4c7d0ec08d4c7a7679903 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 22:09:33 -0500 Subject: Add Tuple.dec_eq{,'} --- src/Util/Tuple.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 2dbc592ff..d762e73b9 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -527,6 +527,16 @@ Proof. destruct n; unfold fieldwise; exact _. Defined. +Global Instance dec_eq' {A} {HA : DecidableRel (@eq A)} : forall {n}, DecidableRel (@eq (tuple' A n)) | 10. +Proof. + induction n; typeclasses eauto. +Defined. + +Global Instance dec_eq {A} {HA : DecidableRel (@eq A)} : forall {n}, DecidableRel (@eq (tuple A n)) | 10. +Proof. + destruct n; typeclasses eauto. +Defined. + Section fieldwise_map. Local Arguments map : simpl never. Lemma fieldwise'_map_eq {A A' B B' n} R (f:A -> A') (g:B -> B') (t1:tuple' A n) (t2:tuple' B n) -- cgit v1.2.3