diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-07 22:09:33 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-07 22:09:33 -0500 |
| commit | c58855f90865aae024a4c7d0ec08d4c7a7679903 (patch) | |
| tree | d463dd596d82bde503ccab52351dc75780aad99f /src/Util/Tuple.v | |
| parent | f4b9bf1646e0b37541ebde5b030a90f4c762173b (diff) | |
Add Tuple.dec_eq{,'}
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 10 |
1 files changed, 10 insertions, 0 deletions
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) |