<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">&lt;<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>&gt;</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&#39;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&#39;t need --copatterns, they are on by default.</div><div class="gmail_quote"><br></div><div class="gmail_quote">/ Ulf</div></div></div>