Mercurial > cpdt > repo

comparison src/DepList.v @ 194:063b5741c248

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generic size examples
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 11:21:01 -0500
parents 8f3fc56b90d4
children b4ea71b6bf94
comparison
equal deleted inserted replaced
193:8e9499e27b6c 194:063b5741c248
78 match n return ilist n -> ilist n -> ilist n with 78 match n return ilist n -> ilist n -> ilist n with
79 | O => fun _ _ => inil 79 | O => fun _ _ => inil
80 | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2)) 80 | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
81 end. 81 end.
82 End map2. 82 End map2.
83
84 Section fold.
85 Variable B : Type.
86 Variable f : A -> B -> B.
87 Variable i : B.
88
89 Fixpoint foldr (n : nat) : ilist n -> B :=
90 match n return ilist n -> B with
91 | O => fun _ => i
92 | S n' => fun ils => f (hd ils) (foldr n' (tl ils))
93 end.
94 End fold.
83 End ilist. 95 End ilist.
96
97 Implicit Arguments inil [A].
98 Implicit Arguments icons [A n].
84 99
85 Implicit Arguments icons [A n]. 100 Implicit Arguments icons [A n].
86 Implicit Arguments get [A n]. 101 Implicit Arguments get [A n].
87 Implicit Arguments map2 [A n]. 102 Implicit Arguments map2 [A n].
103 Implicit Arguments foldr [A B n].
88 104
89 Section hlist. 105 Section hlist.
90 Variable A : Type. 106 Variable A : Type.
91 Variable B : A -> Type. 107 Variable B : A -> Type.
92 108
128 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) := 144 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
129 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with 145 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
130 | nil => fun _ hls2 => hls2 146 | nil => fun _ hls2 => hls2
131 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2) 147 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
132 end. 148 end.
149
150 Variable f : forall x, B x.
151
152 Fixpoint hmake (ls : list A) : hlist ls :=
153 match ls return hlist ls with
154 | nil => hnil
155 | x :: ls' => hcons _ (f x) (hmake ls')
156 end.
133 End hlist. 157 End hlist.
134 158
135 Implicit Arguments hnil [A B]. 159 Implicit Arguments hnil [A B].
136 Implicit Arguments hcons [A B x ls]. 160 Implicit Arguments hcons [A B x ls].
137 Implicit Arguments hget [A B elm ls]. 161 Implicit Arguments hget [A B elm ls].
138 Implicit Arguments happ [A B ls1 ls2]. 162 Implicit Arguments happ [A B ls1 ls2].
163 Implicit Arguments hmake [A B].
139 164
140 Implicit Arguments hfirst [A elm x ls]. 165 Implicit Arguments hfirst [A elm x ls].
141 Implicit Arguments hnext [A elm x ls]. 166 Implicit Arguments hnext [A elm x ls].
142 167
143 Infix ":::" := hcons (right associativity, at level 60). 168 Infix ":::" := hcons (right associativity, at level 60).