Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
196:b4ea71b6bf94 197:f6293ba66559
205 205
206 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1), 206 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
207 hmap h1 +++ hmap h2 = hmap (h1 +++ h2). 207 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
208 induction ls1; crush. 208 induction ls1; crush.
209 Qed. 209 Qed.
210
211 Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls),
212 hget (hmap hls) m = f (hget hls m).
213 induction ls; crush.
214 case a1; crush.
215 Qed.
210 End hmap. 216 End hmap.
211 217
212 Implicit Arguments hmap [A B1 B2 ls]. 218 Implicit Arguments hmap [A B1 B2 ls].