Discussion:
[Agda] Disable post projections?
Martin Escardo
2018-10-24 13:17:04 UTC
Permalink
Is there a way of disabling post projections?

I would prefer the interactive mode to generate pre projections in my case.

Thanks,
Martin
Miëtek Bak
2018-10-30 19:47:02 UTC
Permalink
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)
Post by Martin Escardo
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
https://lists.chalmers.se/mailman/listinfo/agda
Jesper Cockx
2018-10-31 08:31:24 UTC
Permalink
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
Post by Miëtek Bak
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)
Post by Martin Escardo
Is there a way of disabling post projections?
I would prefer the interactive mode to generate pre projections in my
case.
Post by Martin Escardo
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Martin Escardo
2018-10-31 08:38:46 UTC
Permalink
Post by 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.
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
Post by Jesper Cockx
-- Jesper
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)
Post by Martin Escardo
Is there a way of disabling post projections?
I would prefer the interactive mode to generate pre projections
in my case.
Post by Martin Escardo
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Guillaume Brunerie
2018-10-31 14:19:38 UTC
Permalink
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
Post by Martin Escardo
Post by 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.
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
Post by Jesper Cockx
-- Jesper
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)
Post by Martin Escardo
Is there a way of disabling post projections?
I would prefer the interactive mode to generate pre projections
in my case.
Post by Martin Escardo
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Jesper Cockx
2018-11-02 11:48:05 UTC
Permalink
Should now be fixed: https://github.com/agda/agda/issues/3356

-- Jesper

On Wed, Oct 31, 2018 at 3:21 PM 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.
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 <
Post by Martin Escardo
Post by 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
Post by Martin Escardo
Post by Jesper Cockx
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.
Post by Martin Escardo
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
Post by Jesper Cockx
-- Jesper
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)
Post by Martin Escardo
Is there a way of disabling post projections?
I would prefer the interactive mode to generate pre projections
in my case.
Post by Martin Escardo
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...