diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-30 14:27:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-30 16:07:44 -0400 |
| commit | 445ff49ade0fd19c81d954f035394aae561d0958 (patch) | |
| tree | c02770625116cf0f81936075f07de7bf8d9b8b84 /src/Util/HList.v | |
| parent | 2a3da2e5ff16a89cc19c1c2dbd809c0be7c26484 (diff) | |
Get rid of list-based Tuple.map
Diffstat (limited to 'src/Util/HList.v')
| -rw-r--r-- | src/Util/HList.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index 1a724f84b..2a135c75c 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -91,11 +91,10 @@ Qed. Lemma map_is_mapt {n A F B} (f : A -> B) {ts : tuple A n} (ls : hlist F ts) : Tuple.map f ts = mapt (fun x _ => f x) ls. Proof. - destruct n as [|n]; [ reflexivity | ]. + destruct n as [|n]; simpl; [ destruct ts; reflexivity | ]. induction n as [|n IHn]; [ reflexivity | ]. - { unfold mapt in *; simpl @mapt' in *. - rewrite <- IHn; clear IHn. - rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. } + { simpl in *; rewrite <- IHn; clear IHn. + reflexivity. } Qed. Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts) @@ -147,7 +146,7 @@ Global Instance mapt_Proper {n A F B} : Proper ((forall_relation (fun x => pointwise_relation _ Logic.eq)) ==> forall_relation (fun ts => Logic.eq ==> Logic.eq)) - (@HList.mapt n A F B). + (@mapt n A F B). Proof. unfold forall_relation, pointwise_relation, respectful. repeat intro; subst; destruct n as [|n]; [ reflexivity | ]. |