That sounds good to me, too. My main complaint is that goals become unreadable with the way things are currently pretty printed.<br><br><div class="gmail_quote">On Mon, May 14, 2012 at 7:54 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br><div class="gmail_quote"><div class="im">On Mon, May 14, 2012 at 11:59 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se" target="_blank">nad@chalmers.se</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>On 2012-05-14 08:51, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This could be mended if for fixops we would consider all module<br>
parameters hidden, whether they are declared as such or not.<br>
</blockquote>
<br></div>
I think we should strive for simplicity and avoid special cases like<br>
this. Perhaps you /can/ currently write A + true, but do you?<br>
<br>
I think the main problem is that the pretty-printer sometimes writes<br>
A + true. Perhaps we can improve the pretty-printer.</blockquote><div><br></div></div><div>I agree with Nisse here. I think any change to the language would be</div><div>complicating things unduly. Changing the pretty printer to not print</div>
<div>A + true, on the other hand, sounds like a reasonable thing to do.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf </div></font></span></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br>