<div dir="ltr"><div dir="ltr">Should now be fixed: <a href="https://github.com/agda/agda/issues/3356">https://github.com/agda/agda/issues/3356</a></div><div dir="ltr"><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Oct 31, 2018 at 3:21 PM Guillaume Brunerie <<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I’ve noticed that too, sometimes Agda generates postfix projections<br>
even though I never use them and I don’t use --postfix-projections.<br>
Here is an example where C-c C-s generates one:<br>
<br>
open import Agda.Builtin.Equality<br>
<br>
record _×_ (A B : Set) : Set where<br>
  constructor _,_<br>
  field<br>
    fst : A<br>
    snd : B<br>
open _×_<br>
<br>
postulate<br>
  A B : Set<br>
  p : A × B<br>
<br>
eta : p ≡ (? , snd p)<br>
eta= refl<br>
Den ons 31 okt. 2018 kl 09:38 skrev Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>>:<br>
><br>
><br>
><br>
> On 31/10/2018 08:31, <a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a> wrote:<br>
> > I am confused: I always need to *add* the --postfix-projections flag to<br>
> > get Agda to generate my sweet postfix projections (and thus remove the<br>
> > need for parenthesis (parenthesis are horrible)). In what situation does<br>
> > Agda generate postfix projections for you? The only place where I can<br>
> > think of is in pattern-matching lambdas, where there is really no choice.<br>
><br>
> I use pr1 and pr2 for the Sigma projections as in the HoTT Book in my<br>
> HoTT/UF development, and I want to write pr1 z and pr2 z (which I do)<br>
> rather z.pr1 and z.pr2, which also conforms with the usual practice of<br>
> the HoTT Book as well as general mathematical practice. And which also<br>
> goes well with my taste for sour things in preference for sweets,<br>
> including coffee without sugar. :-)<br>
><br>
> But the emacs Agda interactive mode generates them postfix, without me<br>
> adding the --postfix-projections option in my files or anywhere else.<br>
><br>
> Martin<br>
><br>
> ><br>
> > -- Jesper<br>
> ><br>
> > On Tue, Oct 30, 2018 at 8:47 PM Miëtek Bak <<a href="mailto:mietek@bak.io" target="_blank">mietek@bak.io</a><br>
> > <mailto:<a href="mailto:mietek@bak.io" target="_blank">mietek@bak.io</a>>> wrote:<br>
> ><br>
> >     There is still room for one more overloading of `.`!<br>
> ><br>
> >     We are already using `foo . bar`, `foo.bar`, and `foo .bar` — with<br>
> >     the prefix `.` being used for irrelevancy annotations, names that<br>
> >     are not in scope, postfix projections, and probably a dozen other<br>
> >     things that I have either forgotten or never learned.  Could we not<br>
> >     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<br>
> >     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> <mailto:<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> <mailto:<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>
> ><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>
><br>
> --<br>
> Martin Escardo<br>
> <a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</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>