Mercurial > cpdt > repo

comparison src/DepList.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents 0ce9829efa3b
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
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 Arguments INil [A]. 110 Arguments INil {A}.
111 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 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] f ls. 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