<div dir="ltr">And if you attach the where to a function with a parameter, it will be a parametrized module, since the function parameters will be visible.</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Apr 23, 2013 at 12:01 PM, Guillaume Brunerie <span dir="ltr">&lt;<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@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">Here is an example:<br>
<br>
n : ℕ<br>
n = m module foo where<br>
  m : ℕ<br>
  m = 42<br>
<br>
k : ℕ<br>
k = foo.m<br>
<br>
theorem : k ≡ n<br>
theorem = refl<br>
<br>
<br>
Guillaume<br>
<br>
2013/4/23 Owen &lt;<a href="mailto:ellbur@gmail.com">ellbur@gmail.com</a>&gt;:<br>
<div class="HOEnZb"><div class="h5">&gt; Could you provide an example of naming the `where` module? This is a<br>
&gt; feature I have been looking for for awhile as it is helpful for<br>
&gt; writing proofs that relate to functions with `where` clauses, but I<br>
&gt; can&#39;t find any documentation on it.<br>
&gt;<br>
&gt; Best,<br>
&gt; Owen<br>
&gt;<br>
&gt;&gt; Yeah, you can actually even name the where module, too writing &quot;module foo<br>
&gt;&gt; where&quot; attached to a function.<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; On Fri, Apr 19, 2013 at 12:58 PM, Andreas Abel &lt;andreas.abel at <a href="http://ifi.lmu.de" target="_blank">ifi.lmu.de</a>&gt;wrote:<br>
&gt;&gt;<br>
&gt;&gt; &gt; As far as I know, `where&#39; clauses are translated to a module and treated<br>
&gt;&gt; &gt; as mutually recursive with the function they belong to.  This comment about<br>
&gt;&gt; &gt; &#39;let&#39; must be really old.<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; Cheers,<br>
&gt;&gt; &gt; Andreas<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; On 19.04.2013 17:21, Andrés Sicard-Ramírez wrote:<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt;&gt; Hi,<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; Peyton Jones [1, §4.2.8] states that where clauses are translated into<br>
&gt;&gt; &gt;&gt; let expressions.<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; I found the following comment in Agda source code<br>
&gt;&gt; &gt;&gt; (Agda.Syntax.Abstract):<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; -- | We could throw away @where@ clauses at this point and translate<br>
&gt;&gt; &gt;&gt; them to<br>
&gt;&gt; &gt;&gt; --   @let at . It&#39;s not obvious how to remember that the @let@ was really a<br>
&gt;&gt; &gt;&gt; --   @where@ clause though, so for the time being we keep it here.<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; So, are where clauses translated to let expressions in Agda?<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; [1] Simon L. Peyton Jones. The Implementation of Functional<br>
&gt;&gt; &gt;&gt;      Programming Languages. Prentice-Hall International, 1987.<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; Thanks,<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; --<br>
&gt;&gt; &gt;&gt; Andrés<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt; ______________________________**_________________<br>
&gt;&gt; &gt;&gt; Agda mailing list<br>
&gt;&gt; &gt;&gt; Agda at <a href="http://lists.chalmers.se" target="_blank">lists.chalmers.se</a><br>
&gt;&gt; &gt;&gt; <a href="https://lists.chalmers.se/**mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/**mailman/listinfo/agda</a>&lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>&gt;<br>

&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;&gt;<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; --<br>
&gt;&gt; &gt; Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; Theoretical Computer Science, University of Munich<br>
&gt;&gt; &gt; Oettingenstr. 67, D-80538 Munich, GERMANY<br>
&gt;&gt; &gt;<br>
&gt;&gt; &gt; andreas.abel at <a href="http://ifi.lmu.de" target="_blank">ifi.lmu.de</a><br>
&gt;&gt; &gt; <a href="http://www2.tcs.ifi.lmu.de/~**abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~**abel/</a> &lt;<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a>&gt;<br>

&gt;&gt; &gt; ______________________________**_________________<br>
&gt;&gt; &gt; Agda mailing list<br>
&gt;&gt; &gt; Agda at <a href="http://lists.chalmers.se" target="_blank">lists.chalmers.se</a><br>
&gt;&gt; &gt; <a href="https://lists.chalmers.se/**mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/**mailman/listinfo/agda</a>&lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>&gt;<br>

&gt;&gt; &gt;<br>
&gt;&gt; -------------- next part --------------<br>
&gt;&gt; An HTML attachment was scrubbed...<br>
&gt;&gt; URL: <a href="http://lists.chalmers.se/pipermail/agda/attachments/20130419/e1a4b0f2/attachment.html" target="_blank">http://lists.chalmers.se/pipermail/agda/attachments/20130419/e1a4b0f2/attachment.html</a><br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><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>
</div></div></blockquote></div><br></div>