Oh! I had no idea this was even valid syntax. It&#39;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">&lt;<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>&gt;</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">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">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><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><font color="#888888"><div>/ Ulf</div></font></div>
</blockquote></div><br></div>