<br><div class="gmail_quote">On Thu, Jun 16, 2011 at 10:51 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">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>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><div>/ Ulf</div></div>