Mercurial > cpdt > repo
comparison src/DepList.v @ 568:81d63d9c1cc5
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]. |