[Agda] Mutual data definitions
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Jan 27 10:09:13 CET 2015
Of course, the current error message is misleading. Anyone want to
drill around in Agda.Syntax.Concrete.Definitions to make it better?
--Andreas
On 27.01.2015 09:58, Dominique Devriese wrote:
> 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list