Mercurial > cpdt > repo
comparison src/DepList.v @ 569:0ce9829efa3b
Back to working in Coq 8.4
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 20 Jan 2019 15:28:23 -0500 |
parents | 81d63d9c1cc5 |
children | 1dc1d41620b6 |
comparison
equal
deleted
inserted
replaced
568:81d63d9c1cc5 | 569:0ce9829efa3b |
---|---|
196 end; crush. | 196 end; crush. |
197 Qed. | 197 Qed. |
198 End hlist. | 198 End hlist. |
199 | 199 |
200 Arguments HNil [A B]. | 200 Arguments HNil [A B]. |
201 Arguments HCons [A B x ls]. | 201 Arguments HCons [A B x ls] _ _. |
202 Arguments hmake [A B]. | 202 Arguments hmake [A B] f ls. |
203 | 203 |
204 Arguments HFirst [A elm ls]. | 204 Arguments HFirst [A elm ls]. |
205 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 Arguments hmap [A B1 B2] f [ls]. | 236 Arguments hmap [A B1 B2] f [ls] hl. |