[Agda] new style mutual data broken?

[Adam Gundry]

Hi Peter,

On 23/01/13 09:51, Peter Divianszky wrote:
> 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".

When separating declarations and definitions, you are not allowed to
repeat the declaration, otherwise Agda treats them as separate (and
hence the first M has no definition). This will be accepted:

   data L : Set
   data M : Set

   data L where
     nil : L
     y : M → L

   data M where
     x : L → M

Note the lack of ": Set" on the data definitions.

Best regards,

Adam


-- 
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.