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/IffT.v | |
| parent | f929cd20f82206be0bdf40b91c179dcb346408e1 (diff) | |
Rename iffT, add some lemmas about tuple and hlist
Some lemmas admitted
Diffstat (limited to 'src/Util/IffT.v')
| -rw-r--r-- | src/Util/IffT.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/Util/IffT.v b/src/Util/IffT.v index fd132fbfa..f4eaa9d53 100644 --- a/src/Util/IffT.v +++ b/src/Util/IffT.v @@ -1,9 +1,10 @@ Require Import Coq.Classes.RelationClasses. -Notation iffT := (fun A B => inhabited ((A -> B) * (B -> A)))%type. +Notation iffT A B := (((A -> B) * (B -> A)))%type. +Notation iffTp := (fun A B => inhabited (iffT A B)). -Global Instance iffT_Reflexive : Reflexive iffT | 1. +Global Instance iffTp_Reflexive : Reflexive iffTp | 1. Proof. repeat constructor; intro; assumption. Defined. -Global Instance iffT_Symmetric : Symmetric iffT | 1. +Global Instance iffTp_Symmetric : Symmetric iffTp | 1. Proof. repeat (intros [?] || intro); constructor; tauto. Defined. -Global Instance iffT_Transitive : Transitive iffT | 1. +Global Instance iffTp_Transitive : Transitive iffTp | 1. Proof. repeat (intros [?] || intro); constructor; tauto. Defined. |