[Agda] trouble with let and where

[Nicolas Pouillard]

On 11/30/2015 02:26 PM, Andreas Abel wrote:
> Hi Peter & folks,

Hi all,

[...]

> To implement your suggestion,
>
>    where
>      (x , y) = e
>
> we could do similar as for `let` and interpret this as
>
>    where
>      x,y = e    -- x,y is a private identifier for sharing e's evaluation
>      x   = fst x,y
>      y   = snd x,y

I'm wondering if this is any different but I would suggest the following 
translation:

   where
     open Σ e renaming (proj₁ to x; proj₂ to y)

-- 
Best regards,
-- NP