[Agda] Mutual data definitions
Dominique Devriese
dominique.devriese at cs.kuleuven.be
Tue Jan 27 09:58:39 CET 2015
James,
Thanks, I missed this subtlety in the docs!
Dominique
2015-01-27 9:54 GMT+01:00 James Chapman <james at cs.ioc.ee>:
> Hi,
>
> You should omit the type in the 'definition' of B:
>
> data B : Set
>
> data A : Set where
> bA : B → A
>
> data B where
> aB : A → B
> b : B
>
> James
>
>
> On Tue Jan 27 2015 at 10:50:47 AM Dominique Devriese
> <dominique.devriese at cs.kuleuven.be> wrote:
>>
>> Hi all,
>>
>> Can anyone tell me if the following is supposed to work, or if I
>> should use old-style mutual blocks for this? Or maybe I've forgotten
>> something else? I currently get an error about a missing definition
>> for B.
>>
>> data B : Set
>>
>> data A : Set where
>> bA : B → A
>>
>> data B : Set where
>> aB : A → B
>> b : B
>>
>> Thanks,
>> Dominique
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list