[Agda] new style mutual data broken?
adam.gundry at strath.ac.uk
Wed Jan 23 12:08:37 CET 2013
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.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.
More information about the Agda