[Agda] Disable post projections?

[Jesper Cockx]

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.

-- Jesper

On Tue, Oct 30, 2018 at 8:47 PM Miëtek Bak <mietek at bak.io> wrote:

> There is still room for one more overloading of `.`!
>
> 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`?…
>
> I would like to second Martin’s question.
>
> --
> (mb)
>
>
> On Wed, Oct 24, 2018, at 13:17, Martin Escardo wrote:
> > Is there a way of disabling post projections?
> >
> > I would prefer the interactive mode to generate pre projections in my
> case.
> >
> > Thanks,
> > Martin
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181031/33f8d257/attachment.html>