[Agda] `where' scope

Serge D. Mechveliani mechvel at botik.ru
Tue Sep 25 11:35:26 CEST 2012

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.


> 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- MAlonzo  reports a  multiple definition of  f.

More information about the Agda mailing list