Mercurial > cpdt > repo

comparison src/DepList.v @ 196:b4ea71b6bf94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
size_positive
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 13:38:34 -0500
parents 063b5741c248
children f6293ba66559
comparison
equal deleted inserted replaced
195:3676acc40ce1 196:b4ea71b6bf94
99 99
100 Implicit Arguments icons [A n]. 100 Implicit Arguments icons [A n].
101 Implicit Arguments get [A n]. 101 Implicit Arguments get [A n].
102 Implicit Arguments map2 [A n]. 102 Implicit Arguments map2 [A n].
103 Implicit Arguments foldr [A B n]. 103 Implicit Arguments foldr [A B n].
104
105 Section imap.
106 Variables A B : Type.
107 Variable f : A -> B.
108
109 Fixpoint imap (n : nat) : ilist A n -> ilist B n :=
110 match n return ilist A n -> ilist B n with
111 | O => fun _ => inil
112 | S n' => fun ls => icons (f (hd ls)) (imap _ (tl ls))
113 end.
114 End imap.
115
116 Implicit Arguments imap [A B n].
104 117
105 Section hlist. 118 Section hlist.
106 Variable A : Type. 119 Variable A : Type.
107 Variable B : A -> Type. 120 Variable B : A -> Type.
108 121
152 Fixpoint hmake (ls : list A) : hlist ls := 165 Fixpoint hmake (ls : list A) : hlist ls :=
153 match ls return hlist ls with 166 match ls return hlist ls with
154 | nil => hnil 167 | nil => hnil
155 | x :: ls' => hcons _ (f x) (hmake ls') 168 | x :: ls' => hcons _ (f x) (hmake ls')
156 end. 169 end.
170
171 Implicit Arguments hget [ls].
172
173 Theorem hget_hmake : forall ls (m : member ls),
174 hget (hmake ls) m = f elm.
175 induction ls; crush.
176 case a0; reflexivity.
177 Qed.
157 End hlist. 178 End hlist.
158 179
159 Implicit Arguments hnil [A B]. 180 Implicit Arguments hnil [A B].
160 Implicit Arguments hcons [A B x ls]. 181 Implicit Arguments hcons [A B x ls].
161 Implicit Arguments hget [A B elm ls]. 182 Implicit Arguments hget [A B elm ls].