Mercurial > cpdt > repo

diff src/DepList.v @ 197:f6293ba66559

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
map_id
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 14:10:23 -0500
parents b4ea71b6bf94
children f8bcd33bdd91
line wrap: on
line diff
--- a/src/DepList.v	Fri Nov 28 13:38:34 2008 -0500
+++ b/src/DepList.v	Fri Nov 28 14:10:23 2008 -0500
@@ -207,6 +207,12 @@
     hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
     induction ls1; crush.
   Qed.
+
+  Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls),
+    hget (hmap hls) m = f (hget hls m).
+    induction ls; crush.
+    case a1; crush.
+  Qed.
 End hmap.
 
 Implicit Arguments hmap [A B1 B2 ls].