[Agda] Re: `data'-record field overlap

[Francesco Mazzoli]

At Sat, 10 Nov 2012 11:49:36 +0000,
Francesco Mazzoli wrote:
> Looks like a bug, you don't need records or data.  This works:
> 
>     module Foo where
>       foo : Bool
>       foo = true
> 
>     foo : Bool
>     foo = true
> 
> This doesn't:    
> 
>     foo : Bool
>     foo = true
> 
>     module Foo where
>       foo : Bool
>       foo = true

My bad, in the second instance the nested `foo' does indeed clash with the top
one.  I guess I'm just not used to nested modules.

Francesco.