<div dir="ltr"><div>I am confused: I always need to *add* the --postfix-projections flag to get Agda to generate my sweet postfix projections (and thus remove the need for parenthesis (parenthesis are horrible)). In what situation does Agda generate postfix projections for you? The only place where I can think of is in pattern-matching lambdas, where there is really no choice.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, Oct 30, 2018 at 8:47 PM Miëtek Bak <<a href="mailto:mietek@bak.io">mietek@bak.io</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">There is still room for one more overloading of `.`!<br>
<br>
We are already using `foo . bar`, `foo.bar`, and `foo .bar` — with the prefix `.` being used for irrelevancy annotations, names that are not in scope, postfix projections, and probably a dozen other things that I have either forgotten or never learned.  Could we not find some use for `foo. bar`?…<br>
<br>
I would like to second Martin’s question.<br>
<br>
-- <br>
(mb)<br>
<br>
<br>
On Wed, Oct 24, 2018, at 13:17, Martin Escardo wrote:<br>
> Is there a way of disabling post projections?<br>
> <br>
> I would prefer the interactive mode to generate pre projections in my case.<br>
> <br>
> Thanks,<br>
> Martin<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>