[Agda] Mutual data definitions
James Chapman
james at cs.ioc.ee
Tue Jan 27 09:54:45 CET 2015
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150127/e38054f2/attachment.html
More information about the Agda
mailing list