[Agda] Mutual data definitions

[Dominique Devriese]

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