[Agda] Disable post projections?

[Guillaume Brunerie]

I’ve noticed that too, sometimes Agda generates postfix projections
even though I never use them and I don’t use --postfix-projections.
Here is an example where C-c C-s generates one:

open import Agda.Builtin.Equality

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

postulate
  A B : Set
  p : A × B

eta : p ≡ (? , snd p)
eta= refl
Den ons 31 okt. 2018 kl 09:38 skrev Martin Escardo <m.escardo at cs.bham.ac.uk>:
>
>
>
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda