Mercurial > cpdt > repo

comparison src/DepList.v @ 568:81d63d9c1cc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port to Coq 8.9.0
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:16:29 -0500
parents ed829eaa91b2
children 0ce9829efa3b
comparison
equal deleted inserted replaced
567:ec0ce5129fc4 568:81d63d9c1cc5
105 | ICons _ x il' => f x (foldr il') 105 | ICons _ x il' => f x (foldr il')
106 end. 106 end.
107 End fold. 107 End fold.
108 End ilist. 108 End ilist.
109 109
110 Implicit Arguments INil [A]. 110 Arguments INil [A].
111 Implicit Arguments First [n]. 111 Arguments First [n].
112 112
113 Section imap. 113 Section imap.
114 Variables A B : Type. 114 Variables A B : Type.
115 Variable f : A -> B. 115 Variable f : A -> B.
116 116
195 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E 195 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
196 end; crush. 196 end; crush.
197 Qed. 197 Qed.
198 End hlist. 198 End hlist.
199 199
200 Implicit Arguments HNil [A B]. 200 Arguments HNil [A B].
201 Implicit Arguments HCons [A B x ls]. 201 Arguments HCons [A B x ls].
202 Implicit Arguments hmake [A B]. 202 Arguments hmake [A B].
203 203
204 Implicit Arguments HFirst [A elm ls]. 204 Arguments HFirst [A elm ls].
205 Implicit Arguments HNext [A elm x ls]. 205 Arguments HNext [A elm x ls].
206 206
207 Infix ":::" := HCons (right associativity, at level 60). 207 Infix ":::" := HCons (right associativity, at level 60).
208 Infix "+++" := happ (right associativity, at level 60). 208 Infix "+++" := happ (right associativity, at level 60).
209 209
210 Section hmap. 210 Section hmap.
231 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E 231 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
232 end; crush. 232 end; crush.
233 Qed. 233 Qed.
234 End hmap. 234 End hmap.
235 235
236 Implicit Arguments hmap [A B1 B2 ls]. 236 Arguments hmap [A B1 B2] f [ls].