Mercurial > cpdt > repo

comparison src/DepList.v @ 569:0ce9829efa3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.