<div dir="ltr">Yeah, you can actually even name the where module, too writing "module foo where" attached to a function.</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Apr 19, 2013 at 12:58 PM, 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">As far as I know, `where' clauses are translated to a module and treated as mutually recursive with the function they belong to. This comment about 'let' must be really old.<br>
<br>
Cheers,<br>
Andreas<div><div class="h5"><br>
<br>
On 19.04.2013 17:21, Andrés Sicard-Ramírez wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Hi,<br>
<br>
Peyton Jones [1, §4.2.8] states that where clauses are translated into<br>
let expressions.<br>
<br>
I found the following comment in Agda source code<br>
(Agda.Syntax.Abstract):<br>
<br>
-- | We could throw away @where@ clauses at this point and translate them to<br>
-- @let@. It's not obvious how to remember that the @let@ was really a<br>
-- @where@ clause though, so for the time being we keep it here.<br>
<br>
So, are where clauses translated to let expressions in Agda?<br>
<br>
[1] Simon L. Peyton Jones. The Implementation of Functional<br>
Programming Languages. Prentice-Hall International, 1987.<br>
<br>
Thanks,<br>
<br>
--<br>
Andrés<br>
<br>
<br></div></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>