diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-07 14:53:26 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-07 14:53:26 -0500 |
| commit | 2dd39060683127c0f89f35fe8de6ed09b526ce93 (patch) | |
| tree | 650c1fec8ea9f64dba09ebf431622802af1ecaf9 /src/Util/HList.v | |
| parent | 619ab2496a3872cdda1b8f480dc79aa71fa4ae1d (diff) | |
Add map_is_mapt'
Diffstat (limited to 'src/Util/HList.v')
| -rw-r--r-- | src/Util/HList.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index 120d898d9..1a23f8fd6 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -59,3 +59,7 @@ Proof. rewrite <- IHn; clear IHn. rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. } Qed. + +Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts) + : Tuple.map f ts = mapt' (fun x _ => f x) ls. +Proof. apply (@map_is_mapt (S n)). Qed. |