[Agda] `where' scope

[Nils Anders Danielsson]

On 2012-09-25 10:49, Andreas Abel wrote:
> Sounds like a bug in MAlonzo, can you report it on the bug tracker?

No, this is intentional (and has nothing to do with MAlonzo): some forms
of shadowing are not allowed. Perhaps we should change the rules,
though. See issue 359:

   What should the rules for shadowing be?
   http://code.google.com/p/agda/issues/detail?id=359

-- 
/NAD