[Agda] new style mutual data broken?

Peter Divianszky divipp at gmail.com
Wed Jan 23 10:51:21 CET 2013


According to release-notes/2-3-0.txt,
the Agda compiler should accept the following declarations:

   data L : Set
   data M : Set

   data L : Set where
     nil : L
     y : M → L

   data M : Set where
     x : L → M

but it gives the error message "Missing definition for M".

Should I open a bug ticket?


More information about the Agda mailing list