Oh! I had no idea this was even valid syntax. It's good to know, but yeah, I guess the proof is impossible until the standard lib can be updated to use this pattern?<div><br></div><div>Thanks,</div><div>Dan<br><br><div class="gmail_quote">
On Thu, Jun 16, 2011 at 6:44 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com">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 Thu, Jun 16, 2011 at 10:51 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
In the back of my mind I remember from some Agda meeting talk that<br>
<br>
bla : _<br>
bla = ...<br>
where blurp = ...<br>
<br>
allows one to access blurp as<br>
<br>
bla.blurp<br>
<br>
But that does not seem to be the case...<br>
<br>
@Ulf: Did such a feature exist at some time?<br></blockquote><div><br></div></div><div>Yes, and it still does, but it requires that you name the where block.</div><div><br></div><div>bla : _</div><div>bla = ...</div><div>
module BlaLocal where</div>
<div> blurp = ...</div><div><br></div><div>let's you access blurp as BlaLocal.blurp. The reason you have to name it is that</div><div>you can have several where blocks for the same definition (one for each clause),</div>
<div>so it's not clear how to name them automatically.</div><div><br></div><font color="#888888"><div>/ Ulf</div></font></div>
</blockquote></div><br></div>