From 2dd39060683127c0f89f35fe8de6ed09b526ce93 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 7 Nov 2016 14:53:26 -0500 Subject: Add map_is_mapt' --- src/Util/HList.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Util/HList.v') 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. -- cgit v1.2.3