<br><div class="gmail_quote">On Thu, Jun 16, 2011 at 10:51 AM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;</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&#39;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&#39;s not clear how to name them automatically.</div><div><br></div><div>/ Ulf</div></div>