[Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect

Ulf Norell ulf.norell at gmail.com
Mon May 14 13:54:25 CEST 2012

On Mon, May 14, 2012 at 11:59 AM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> On 2012-05-14 08:51, Andreas Abel wrote:
>> This could be mended if for fixops we would consider all module
>> parameters hidden, whether they are declared as such or not.
> I think we should strive for simplicity and avoid special cases like
> this. Perhaps you /can/ currently write A + true, but do you?
> I think the main problem is that the pretty-printer sometimes writes
> A + true. Perhaps we can improve the pretty-printer.

I agree with Nisse here. I think any change to the language would be
complicating things unduly. Changing the pretty printer to not print
A + true, on the other hand, sounds like a reasonable thing to do.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120514/f67709c0/attachment.html

More information about the Agda mailing list