diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-08 11:22:11 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-08 11:22:11 -0500 |
| commit | 853821e4374050d5a770ee623b24a7bf15e288ae (patch) | |
| tree | cec7afb052b974bc081618ae5ab5a4275800cd30 /src/Util/Prod.v | |
| parent | f929cd20f82206be0bdf40b91c179dcb346408e1 (diff) | |
Rename iffT, add some lemmas about tuple and hlist
Some lemmas admitted
Diffstat (limited to 'src/Util/Prod.v')
| -rw-r--r-- | src/Util/Prod.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Util/Prod.v b/src/Util/Prod.v index fea2589be..bcd9404a6 100644 --- a/src/Util/Prod.v +++ b/src/Util/Prod.v @@ -76,23 +76,23 @@ Proof. repeat (intros [? ?] || intro || split); assumption. Defined. Global Instance iff_prod_Proper : Proper (iff ==> iff ==> iff) (fun A B => prod A B). Proof. repeat intro; tauto. Defined. -Global Instance iff_iffT_prod_Proper - : Proper (iff ==> iffT ==> iffT) (fun A B => prod A B) | 1. +Global Instance iff_iffTp_prod_Proper + : Proper (iff ==> iffTp ==> iffTp) (fun A B => prod A B) | 1. Proof. intros ?? [?] ?? [?]; constructor; tauto. Defined. -Global Instance iffT_iff_prod_Proper - : Proper (iffT ==> iff ==> iffT) (fun A B => prod A B) | 1. +Global Instance iffTp_iff_prod_Proper + : Proper (iffTp ==> iff ==> iffTp) (fun A B => prod A B) | 1. Proof. intros ?? [?] ?? [?]; constructor; tauto. Defined. -Global Instance iffT_iffT_prod_Proper - : Proper (iffT ==> iffT ==> iffT) (fun A B => prod A B) | 1. +Global Instance iffTp_iffTp_prod_Proper + : Proper (iffTp ==> iffTp ==> iffTp) (fun A B => prod A B) | 1. Proof. intros ?? [?] ?? [?]; constructor; tauto. Defined. -Hint Extern 2 (Proper _ prod) => apply iffT_iffT_prod_Proper : typeclass_instances. -Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffT_prod_Proper : typeclass_instances. +Hint Extern 2 (Proper _ prod) => apply iffTp_iffTp_prod_Proper : typeclass_instances. +Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffTp_prod_Proper : typeclass_instances. Hint Extern 2 (Proper _ (fun A B => prod A B)) => refine iff_prod_Proper : typeclass_instances. (** ** Useful Tactics *) |