[Agda] Disable post projections?

[Jesper Cockx]

Should now be fixed: https://github.com/agda/agda/issues/3356

-- Jesper

On Wed, Oct 31, 2018 at 3:21 PM Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181102/6e94cc8d/attachment.html>