[Agda] Where clauses

[Daniel Peebles]

Yeah, you can actually even name the where module, too writing "module foo
where" attached to a function.


On Fri, Apr 19, 2013 at 12:58 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> 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.
>
> Cheers,
> Andreas
>
>
> On 19.04.2013 17:21, Andrés Sicard-Ramírez wrote:
>
>> Hi,
>>
>> Peyton Jones [1, §4.2.8] states that where clauses are translated into
>> let expressions.
>>
>> I found the following comment in Agda source code
>> (Agda.Syntax.Abstract):
>>
>> -- | We could throw away @where@ clauses at this point and translate
>> them to
>> --   @let at . It's not obvious how to remember that the @let@ was really a
>> --   @where@ clause though, so for the time being we keep it here.
>>
>> So, are where clauses translated to let expressions in Agda?
>>
>> [1] Simon L. Peyton Jones. The Implementation of Functional
>>      Programming Languages. Prentice-Hall International, 1987.
>>
>> Thanks,
>>
>> --
>> Andrés
>>
>>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130419/e1a4b0f2/attachment.html