[Agda] Where clauses
ellbur at gmail.com
Tue Apr 23 10:41:37 CEST 2013
Could you provide an example of naming the `where` module? This is a
feature I have been looking for for awhile as it is helpful for
writing proofs that relate to functions with `where` clauses, but I
can't find any documentation on it.
> 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?
> >>  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
More information about the Agda