<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"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></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 <<a href="mailto:ellbur@gmail.com">ellbur@gmail.com</a>>:<br>
<div class="HOEnZb"><div class="h5">> Could you provide an example of naming the `where` module? This is a<br>
> feature I have been looking for for awhile as it is helpful for<br>
> writing proofs that relate to functions with `where` clauses, but I<br>
> can't find any documentation on it.<br>
><br>
> Best,<br>
> Owen<br>
><br>
>> Yeah, you can actually even name the where module, too writing "module foo<br>
>> where" attached to a function.<br>
>><br>
>><br>
>> On Fri, Apr 19, 2013 at 12:58 PM, Andreas Abel <andreas.abel at <a href="http://ifi.lmu.de" target="_blank">ifi.lmu.de</a>>wrote:<br>
>><br>
>> > As far as I know, `where' clauses are translated to a module and treated<br>
>> > as mutually recursive with the function they belong to. This comment about<br>
>> > 'let' must be really old.<br>
>> ><br>
>> > Cheers,<br>
>> > Andreas<br>
>> ><br>
>> ><br>
>> > On 19.04.2013 17:21, Andrés Sicard-Ramírez wrote:<br>
>> ><br>
>> >> 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<br>
>> >> them to<br>
>> >> -- @let at . 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>
>> >> ______________________________**_________________<br>
>> >> Agda mailing list<br>
>> >> Agda at <a href="http://lists.chalmers.se" target="_blank">lists.chalmers.se</a><br>
>> >> <a href="https://lists.chalmers.se/**mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/**mailman/listinfo/agda</a><<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>><br>
>> >><br>
>> >><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>
>> > andreas.abel at <a href="http://ifi.lmu.de" target="_blank">ifi.lmu.de</a><br>
>> > <a href="http://www2.tcs.ifi.lmu.de/~**abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~**abel/</a> <<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a>><br>
>> > ______________________________**_________________<br>
>> > Agda mailing list<br>
>> > Agda at <a href="http://lists.chalmers.se" target="_blank">lists.chalmers.se</a><br>
>> > <a href="https://lists.chalmers.se/**mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/**mailman/listinfo/agda</a><<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>><br>
>> ><br>
>> -------------- next part --------------<br>
>> An HTML attachment was scrubbed...<br>
>> 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>
> _______________________________________________<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>
_______________________________________________<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>