[Agda] new style mutual data broken?
divipp at gmail.com
Wed Jan 23 14:13:29 CET 2013
Thanks, it works with your modification!
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,
More information about the Agda