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

[Andreas Abel]

I stumble over this myself sometimes.  In principle, since module Foo 
does not *use* foo, there is no real ambiguity, and both variants could 
pass.  However, the scope checker already complains if you redefine 
something which is in scope.

Cheers,
Andreas

On 11.11.12 10:19 PM, Francesco Mazzoli wrote:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/