Mercurial > cpdt > repo

comparison src/DepList.v @ 179:8f3fc56b90d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PatMatch Elaborate_correct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 14:12:22 -0500
parents ba306bf9ec80
children 063b5741c248
comparison
equal deleted inserted replaced
178:f41d4e43fd30 179:8f3fc56b90d4
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* Dependent list types presented in Chapter 8 *) 10 (* Dependent list types presented in Chapter 8 *)
11 11
12 Require Import Arith List. 12 Require Import Arith List Tactics.
13 13
14 Set Implicit Arguments. 14 Set Implicit Arguments.
15 15
16 16
17 Section ilist. 17 Section ilist.
152 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls := 152 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
153 match ls return hlist B1 ls -> hlist B2 ls with 153 match ls return hlist B1 ls -> hlist B2 ls with
154 | nil => fun _ => hnil 154 | nil => fun _ => hnil
155 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl) 155 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
156 end. 156 end.
157
158 Implicit Arguments hmap [ls].
159
160 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
161 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
162 induction ls1; crush.
163 Qed.
157 End hmap. 164 End hmap.
158 165
159 Implicit Arguments hmap [A B1 B2 ls]. 166 Implicit Arguments hmap [A B1 B2 ls].