[Agda] Impossible proofs about where blocks?

[Ulf Norell]

On Thu, Jun 16, 2011 at 10:51 AM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> In the back of my mind I remember from some Agda meeting talk that
>
>  bla : _
>  bla = ...
>    where blurp = ...
>
> allows one to access blurp as
>
>  bla.blurp
>
> But that does not seem to be the case...
>
> @Ulf:  Did such a feature exist at some time?
>

Yes, and it still does, but it requires that you name the where block.

bla : _
bla = ...
  module BlaLocal where
    blurp = ...

let's you access blurp as BlaLocal.blurp. The reason you have to name it is
that
you can have several where blocks for the same definition (one for each
clause),
so it's not clear how to name them automatically.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110616/2342ae78/attachment.html