[Agda] `data'-record field overlap

Serge D. Mechveliani mechvel at botik.ru
Sat Nov 10 12:18:16 CET 2012

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?



More information about the Agda mailing list