[Agda] Where clauses

[Guillaume Brunerie]

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