[Agda] Disable post projections?

[Martin Escardo]

On 31/10/2018 08:31, Jesper at sikanda.be wrote:
> 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.

I use pr1 and pr2 for the Sigma projections as in the HoTT Book in my 
HoTT/UF development, and I want to write pr1 z and pr2 z (which I do) 
rather z.pr1 and z.pr2, which also conforms with the usual practice of 
the HoTT Book as well as general mathematical practice. And which also 
goes well with my taste for sour things in preference for sweets, 
including coffee without sugar. :-)

But the emacs Agda interactive mode generates them postfix, without me 
adding the --postfix-projections option in my files or anywhere else.

Martin

> 
> -- Jesper
> 
> On Tue, Oct 30, 2018 at 8:47 PM Miëtek Bak <mietek at bak.io 
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>      > https://lists.chalmers.se/mailman/listinfo/agda
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe