<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 29, 2016 at 2:16 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">You can write eDSet and eUpDSet using copatterns as follows:<br><br><div style="margin-left:40px">eDSet : DSet eDecSetoid<br>dSet1 eDSet = f<span class="gmail-"><br>
where<br>
f : eC → eC<br>
f = id<br></span></div><div style="margin-left:40px"> dSet2 eDSet = g<br></div><div style="margin-left:40px"> where<br></div><div style="margin-left:40px"><span class="gmail-">
g : eC → ℕ<br>
g _ = 0<br>
<br>eUpDSet : UpDSet _ _<br></span>decSetoid eUpDSet = eDecSetoid <br>dSet eUpDSet = eDSet</div></div></blockquote><div><br></div><div>A nice thing with copatterns is that it lets you do further pattern matching, so in this example (which doesn't use pattern matching, but it could) you can write (patching Jespers code a little to make it check)</div><div><br></div></div></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div class="gmail_extra"><div class="gmail_quote"><div> eDSet : DSet eDecSetoid</div></div></div><div class="gmail_extra"><div class="gmail_quote"><div> DSet.dSet1 eDSet = id</div></div></div><div class="gmail_extra"><div class="gmail_quote"><div> DSet.dset2 eDSet _ = 0</div><div><br></div></div></div><div class="gmail_extra"><div class="gmail_quote"><div> eUpDSet : UpDSet _ _</div></div></div><div class="gmail_extra"><div class="gmail_quote"><div> UpDSet.decSetoid eUpDSet = eDecSetoid</div></div></div><div class="gmail_extra"><div class="gmail_quote"><div> UpDSet.dSet eUpDSet = eDSet -- (2)</div></div></div></blockquote><div class="gmail_extra"><div class="gmail_quote"><div><div style="margin-left:40px"><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"></blockquote></div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"></blockquote><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote><div style="margin-left:40px"><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote><blockquote style="margin:0px 0.8ex;border-left:1px solid rgb(204,204,204);border-right:1px solid rgb(204,204,204);padding-left:1ex;padding-right:1ex" class="gmail_quote "></blockquote></div><div style="margin-left:40px"><div><br></div></div></div>Also you shouldn't need --copatterns, they are on by default.</div><div class="gmail_quote"><br></div><div class="gmail_quote">/ Ulf</div></div></div>