[Agda] Where clauses

[Owen]

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.

Best,
Owen

> 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