[Agda] `where' scope

[Serge D. Mechveliani]

On Tue, Sep 25, 2012 at 10:49:15AM +0200, Andreas Abel wrote:
> Sounds like a bug in MAlonzo, can you report it on the bug tracker?
> Thx, Andreas

I have done it:   http://code.google.com/p/agda/issues/entry
shows a ticket.
It worths now to check the `let' construct similarly.

I have got a bit frightened by this `where' issue. 
And now there is a relief, for if it is a bug, then this can be fixed.

------
Sergei


> On 24.09.12 10:13 PM, Serge D. Mechveliani wrote:
>> People,	
>> how does this occur that `where' does not protect its local scope?
>> Thus, for
>>    f : Nat -> Nat
>>    f = suc
>>    g : Nat -> Nat
>>    g x =  f $ suc x  where
>>                      f : Nat -> Nat
>>                      f y = y
>>
>> Agda-2.3.0.1 MAlonzo  reports a  multiple definition of  f.