[Agda] new style mutual data broken?

[Peter Divianszky]

Thanks, it works with your modification!

Peter

On 01/23/2013 12:08 PM, Adam Gundry wrote:
> 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
>
>