[Agda] Disable post projections?

[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)


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
> https://lists.chalmers.se/mailman/listinfo/agda