[Agda] `data'-record field overlap

Andreas Abel andreas.abel at ifi.lmu.de
Sat Nov 10 15:48:42 CET 2012

Data modules are always opened, so if you uncomment the first line, then 
the second definition of foo within record Foo2 creates ambiguity.

However, record modules are not opened by default.  If you squeeze "open 
Foo2" inbetween the two record declarations, you also get an error.

While constructors can be overloaded, fields cannot (yet).  However, I 
do not think we will add ambiguous identifiers like foo that can both 
denote a constructor and a field.


On 10.11.12 12:18 PM, Serge D. Mechveliani wrote:
> People,
> the program
>    -- data   Foo1 : Set where foo : Bool -> Foo1
>    record Foo2 : Set where field foo : Bool
>    record Foo3 : Set where field foo : Bool
> is accepted in Agda-
> And un-commenting the first line yields the report of a multiple
> definition for  foo.
> May be this is natural.
> Anyway, is this a deliberate language restriction?
> Thanks,
> ------
> Sergei
> _______________________________________________
> 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

More information about the Agda mailing list