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

[Daniel Peebles]

That sounds good to me, too. My main complaint is that goals become
unreadable with the way things are currently pretty printed.

On Mon, May 14, 2012 at 7:54 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

>
> 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
>
> _______________________________________________
> 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/20120514/95fe09e4/attachment.html