Mercurial > cpdt > repo

comparison src/DepList.v @ 163:ba306bf9ec80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Feeling stuck with Hoas
author Adam Chlipala <adamc@hcoop.net>
date Tue, 04 Nov 2008 16:45:50 -0500
parents e70fbfc56c46
children 8f3fc56b90d4
comparison
equal deleted inserted replaced
162:df02642f93b8 163:ba306bf9ec80
140 Implicit Arguments hfirst [A elm x ls]. 140 Implicit Arguments hfirst [A elm x ls].
141 Implicit Arguments hnext [A elm x ls]. 141 Implicit Arguments hnext [A elm x ls].
142 142
143 Infix ":::" := hcons (right associativity, at level 60). 143 Infix ":::" := hcons (right associativity, at level 60).
144 Infix "+++" := happ (right associativity, at level 60). 144 Infix "+++" := happ (right associativity, at level 60).
145
146 Section hmap.
147 Variable A : Type.
148 Variables B1 B2 : A -> Type.
149
150 Variable f : forall x, B1 x -> B2 x.
151
152 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
153 match ls return hlist B1 ls -> hlist B2 ls with
154 | nil => fun _ => hnil
155 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
156 end.
157 End hmap.
158
159 Implicit Arguments hmap [A B1 B2 ls].