[Agda] `where' scope

Nils Anders Danielsson nad at chalmers.se
Tue Sep 25 14:41:28 CEST 2012

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?


More information about the Agda mailing list