<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Sep 29, 2016 at 4:47 PM, Wolfram Kahl <span dir="ltr"><<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">kahl@cas.mcmaster.ca</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"><span class="gmail-">On Wed, Sep 28, 2016 at 03:16:56PM +0200, Nils Anders Danielsson wrote:<br>
> On 2016-09-28 15:07, Andrea Vezzosi wrote:<br>
> >However you should also consider the following version, so that<br>
> >(suc'Rd (rd a n)) does not reduce by itself, but only when projections<br>
> >are applied to it.<br>
> ><br>
</span>> > [...]<br>
<span class="gmail-">><br>
> I think sucRd is more readable than suc'Rd, and I don't think we should<br>
> encourage people to obfuscate their code in order to make it faster. A<br>
> better alternative might be to devise some way to instruct Adga to do<br>
> this kind of rewrite behind the scenes.<br>
<br>
</span>Strongly agreed!<br></blockquote><div><br></div><div>Unless you're using lots of nested sigmas (in which case you're on your own),</div><div>I don't think the main problems are coming from the kind of examples where</div><div>you'd rather use a constructor, but from the big algebraic structure kind of examples</div><div>where copatterns are nicer anyway.</div><div><br></div><div>But of course, feel free to suggest some concrete ideas for what could be done</div><div>behind the scenes and what it would look like in the code. I'm slightly worried that</div><div>people would get surprised by examples like</div><div><br></div><div>{-# MAGIC_REWRITE_INTO_COPATTERNS Σ #-}</div><div><br></div><div>foo : (x , y) ≡ (x , y)</div><div>foo = refl -- error since the two pairs got rewritten into two different copattern definitions</div><div><br></div><div>/ Ulf</div></div></div></div>