[Agda] Where clauses

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Fri Apr 19 19:22:09 CEST 2013


On Fri, Apr 19, 2013 at 11:58 AM, 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.
>
>
Andreas, thanks for the information.

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130419/b3f286e4/attachment.html


More information about the Agda mailing list