[Agda] Where clauses

[Daniel Peebles]

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.


On Tue, Apr 23, 2013 at 12:01 PM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> Here is an example:
>
> n : ℕ
> n = m module foo where
>   m : ℕ
>   m = 42
>
> k : ℕ
> k = foo.m
>
> theorem : k ≡ n
> theorem = refl
>
>
> Guillaume
>
> 2013/4/23 Owen <ellbur at gmail.com>:
> > 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
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130423/98d57f08/attachment.html